mathlib

31f5688a - refactor(ring_theory/valuation/basic): `fun_like` design for `valuation` (#11830)

refactor(ring_theory/valuation/basic): `fun_like` design for `valuation` (#11830) Introduce `valuation_class`, the companion typeclass to `valuation`. Deprecate lemmas. Rename the field from `map_add'` to `map_add_le_max'` to avoid confusion with the eponymous field from `add_hom`.