The Krull dimension of a local ring #
In this file, we proved some results about the Krull dimension of a local ring.
theorem
ringKrullDim_eq_one_iff_of_isLocalRing_isDomain
{R : Type u_1}
[CommRing R]
[IsLocalRing R]
[IsDomain R]
:
ringKrullDim R = 1 ↔ ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical