theorem integrally_closed_noetherian_dim_one_localization_isDVR (A : Type u_1) [CommRing A] [IsDomain A] [IsNoetherianRing A] [Ring.DimensionLEOne A] [IsIntegrallyClosed A] (P : Ideal A) [P.IsPrime] (hP : P ≠ ⊥) : IsDiscreteValuationRing (Localization.AtPrime P)

If $A$ is a Noetherian, integrally closed domain of Krull dimension $\leq 1$ (i.e. a Dedekind domain), then the localization $A_P$ at any nonzero prime $P$ is a discrete valuation ring.