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