mathlib3

cbcbe24d - feat(algebra/ordered_monoid): linear_ordered_add_comm_monoid(_with_top) (#6520)

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` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>