Equivalent conditions for DVR

In DiscreteValuationRing.TFAE, we show that the following are equivalent for a noetherian local domain (R, m, k):

• R is a discrete valuation ring
• R is a valuation ring
• R is a dedekind domain
• R is integrally closed with a unique prime ideal
• m is principal
• dimₖ m/m² = 1
• Every nonzero ideal is a power of m.

theorem exists_maximalIdeal_pow_eq_of_principal (R : Type u_1) [CommRing R] [IsNoetherianRing R] [LocalRing R] [IsDomain R] (h : ¬IsField R) (h' : Submodule.IsPrincipal (LocalRing.maximalIdeal R)) (I : Ideal R) (hI : I ≠ ⊥) : ∃ n, I = LocalRing.maximalIdeal R ^ n

theorem maximalIdeal_isPrincipal_of_isDedekindDomain (R : Type u_1) [CommRing R] [LocalRing R] [IsDomain R] [IsDedekindDomain R] : Submodule.IsPrincipal (LocalRing.maximalIdeal R)

theorem DiscreteValuationRing.TFAE (R : Type u_1) [CommRing R] [IsNoetherianRing R] [LocalRing R] [IsDomain R] (h : ¬IsField R) : List.TFAE [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ Ideal.IsPrime P, Submodule.IsPrincipal (LocalRing.maximalIdeal R), FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = LocalRing.maximalIdeal R ^ n]