# 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.