theorem dim_affine_space_eq (k : Type u_1) [Field k] (n : ℕ) : ringKrullDim (MvPolynomial (Fin n) k) = ↑n

Theorem 5.1: The affine n-space A^n = Spec k[x₁,…,xₙ] has Krull dimension n.

theorem variety_finite_krullDim (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] [Algebra.FiniteType k A] : ringKrullDim A ≠ ⊤

Every finitely generated k-algebra has finite Krull dimension (i.e. not ⊤).