Commit 2020-12-04 15:57 cb7effa8

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.