Commit 2025-07-26 15:56 c238b7e9

feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations (#26623) We prove that the valuation subring of a discretely-valued field is a DVR. Conversely, given a DVR A and a field K satisfying IsFractionRing A K, we show that the valuation induced on K is discrete. We provide the ring isomorphism between a DVR and the valuation subring in its field of fractions endowed with the adic valuation of the maximal ideal.