Commit 2021-05-06 06:18 9154a830
View on Github →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 valuations to add_valuations.