∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [inst_3 : IsDomain R],
  ¬IsField R →
    [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, 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