# Equivalent conditions for DVR #

In DiscreteValuationRing.TFAE, we show that the following are equivalent for a noetherian local domain that is not a field (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.

Also see tfae_of_isNoetherianRing_of_localRing_of_isDomain for a version without ¬ IsField R.

theorem exists_maximalIdeal_pow_eq_of_principal (R : Type u_1) [] [] [] [] (h' : ) (I : ) (hI : I ) :
∃ (n : ), I =
theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain (R : Type u_1) [] [] [] [] :
[, , , ∀ (P : ), P P.IsPrime, , , ∀ (I : ), I ∃ (n : ), I = ].TFAE

Let (R, m, k) be a noetherian local domain (possibly a field). The following are equivalent: 0. R is a PID

1. R is a valuation ring
2. R is a dedekind domain
3. R is integrally closed with at most one non-zero prime ideal
4. m is principal
5. dimₖ m/m² ≤ 1
6. Every nonzero ideal is a power of m.

Also see DiscreteValuationRing.TFAE for a version assuming ¬ IsField R.

theorem DiscreteValuationRing.TFAE (R : Type u_1) [] [] [] [] (h : ¬) :
[, , , ∃! P : , P P.IsPrime, , , ∀ (I : ), I ∃ (n : ), I = ].TFAE

The following are equivalent for a noetherian local domain that is not a field (R, m, k): 0. R is a discrete valuation ring

1. R is a valuation ring
2. R is a dedekind domain
3. R is integrally closed with a unique non-zero prime ideal
4. m is principal
5. dimₖ m/m² = 1
6. Every nonzero ideal is a power of m.

Also see tfae_of_isNoetherianRing_of_localRing_of_isDomain for a version without ¬ IsField R.

@[instance 100]
instance IsDedekindDomain.isPrincipalIdealRing (R : Type u_1) [] [] [] :
Equations
• =