theorem Hauptidealsatz.dim_quotient_ge_dim_minus_one {R : Type u_1} [CommRing R] [IsDomain R] (g : R) (hg : g ≠ 0) : ringKrullDim (R ⧸ Ideal.span {g}) + 1 ≤ ringKrullDim R

For a nonzero element g of a domain R, the Krull dimension drops by at most one when passing to the quotient R/(g).

theorem Hauptidealsatz.height_eq_one_of_mem_minimalPrimes_principal {R : Type u_1} [CommRing R] [IsDomain R] [IsNoetherianRing R] (g : R) (hg : g ≠ 0) (_hg_unit : ¬IsUnit g) (p : Ideal R) [p.IsPrime] (hp : p ∈ (Ideal.span {g}).minimalPrimes) : p.height = 1

Krull's Hauptidealsatz (Thm 5.4, Lec 5): In a Noetherian domain R, every minimal prime over a nonzero non-unit principal ideal (g) has height exactly one. Geometrically, each irreducible component of the zero locus Z(g) has codimension one.