mathlib3

cb7effa8 - feat(ring_theory/discrete_valuation_ring): add additive valuation (#5094)

feat(ring_theory/discrete_valuation_ring): add additive valuation (#5094) Following the approach used for p-adic numbers, we define an additive valuation on a DVR R as a bare function v: R -> nat, with the convention that v(0)=0 instead of +infinity for convenience. Note that we have no `hom` structure (like `monoid_hom` or `add_monoid_hom`) for v(a*b)=v(a)+v(b) and anyway this doesn't even hold if ab=0. We prove all the usual axioms.