mathlib

ad244dd7 - feat(ring_theory/dedekind_domain/adic_valuation): extend valuation (#13462)

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. Co-authored-by: Oliver Nash <github@olivernash.org>