mathlib

9154a830 - feat(algebra/*, ring_theory/valuation/basic): `linear_ordered_add_comm_group_with_top`, `add_valuation.map_sub` (#7452)

feat(algebra/*, ring_theory/valuation/basic): `linear_ordered_add_comm_group_with_top`, `add_valuation.map_sub` (#7452) Defines `linear_ordered_add_comm_group_with_top` Uses that to port a few more facts about `valuation`s to `add_valuation`s.