Commit 2021-03-05 21:45 cbcbe24d
View on Github →feat(algebra/ordered_monoid): linear_ordered_add_comm_monoid(_with_top) (#6520)
Separates out classes for linear_ordered_(add_)comm_monoid
Creates linear_ordered_add_comm_monoid_with_top, an additive and order-reversed version of linear_ordered_comm_monoid_with_zero.
Puts an instance of linear_ordered_add_comm_monoid_with_top on with_top of any linear_ordered_add_comm_monoid and also on enat