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