Commit 2022-02-05 09:52 31f5688a
View on Github →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.