Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-10 20:43 60e25799

View on Github →

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

Estimated changes

added theorem add_valuation.comap_id
added theorem add_valuation.ext
added theorem add_valuation.ext_iff
added theorem add_valuation.map_add
added theorem add_valuation.map_mul
added theorem add_valuation.map_one
added theorem add_valuation.map_pow
added theorem add_valuation.map_zero
added def add_valuation.of
added theorem add_valuation.of_apply
added theorem add_valuation.top_iff
added def add_valuation