Commit 2026-04-16 12:42 3dcb7dd9

feat: localizations of primes in Dedekind domains are valuation subrings (#33010) The goal of this PR is the theorem valuationSubringAtPrime_eq_valuationSubring which states that the localization at a nonzero prime in a Dedekind domain is precisely the valuation subring of the valuation associated with that same prime. Given a Dedekind domain R in its field of fractions K, we define IsDedekindDomain.valuationSubringAtPrime, which is the localization of R at a nonzero prime, viewed as valuation subring of K. We show that valuationSubringAtPrime K v ≤ (valuation K v).valuationSubring and use maximality to show that they must be equal. Other small note:

• added a variant of intValuation_exists_uniformizer in terms of valuation (instead of intValuation).