mathlib3

60e25799 - feat(ring_theory/valuation/basic): additive valuations (#6559)

feat(ring_theory/valuation/basic): additive valuations (#6559) Introduces `add_valuation`, a version of `valuation` that takes values in a `linear_ordered_add_comm_monoid_with_top`. As an example, defines `multiplicity.add_valuation`