theorem maximal_height_eq_of_field (k : Type u_1) [Field k] (n : ℕ) (M : Ideal (MvPolynomial (Fin n) k)) : M.IsMaximal → M.height = ↑n

Helper: in the polynomial ring k[x_1, …, x_n] over a field, every maximal ideal has height exactly n.

theorem hypersurface_dim_n_minus_one (k : Type u_1) [Field k] (n : ℕ) (hn : 0 < n) (f : MvPolynomial (Fin n) k) (hf0 : f ≠ 0) (hfu : ¬IsUnit f) : ringKrullDim (MvPolynomial (Fin n) k ⧸ Ideal.span {f}) = ↑(n - 1)

Hypersurface dimension (Cor 10, Lec 5): a hypersurface in A^n cut out by a single nonzero non-unit polynomial f has dimension n − 1.