mathlib

4150728b - move(algebra/order/monoid/*): Relocate `zero_le_one_class` (#17646)

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. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>