Commit 2022-11-21 08:20 4150728b
View on Github →move(algebra/order/monoid/*): Relocate zero_le_one_class (#17646)
Move zero_le_one_class and linear_ordered_comm_monoid_with_zero to algebra.order.monoid.with_zero. This makes algebra.order.monoid.defs and algebra.order.monoid.canonical.defs not depend on group_with_zero anymore.
And indeed we want to develop the theory of ordered additive and multiplicative monoids before mixing both worlds.