mathlib

4bf4d9df - feat(ring_theory/dedekind_domain/adic_valuation): add adic valuation on a Dedekind domain (#12712)

feat(ring_theory/dedekind_domain/adic_valuation): add adic valuation on a Dedekind domain (#12712) Given a Dedekind domain R of Krull dimension 1 and a maximal ideal v of R, we define the v-adic valuation on R and prove some of its properties, including the existence of uniformizers.