Commit 2022-05-09 11:25 ad244dd7

feat(ring_theory/dedekind_domain/adic_valuation): extend valuation (#13462) We extend the v-adic valuation on a Dedekind domain R to its field of fractions K and prove some basic properties. We define the completion of K with respect to this valuation, as well as its ring of integers, and provide some topological instances.