Commit 2026-03-06 15:35 f2a0d432

feat(RingTheory/DedekindDomain/AdicValuation): values in adic integers have unit denominator (#35724) If R is a Dedekind domain and v a valuation on R, then any v-adic integer in the field of fractions of K can be written as n / d with n d : R and v d = 1. Part of showing R is dense in O_v, which is used to show that R / v is isomorphic to the residue field of O_v and to construct the base change isomorphism for finite adeles.