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.

Estimated changes

added theorem one_le_two'
added theorem one_le_two
added theorem zero_le_four
added theorem zero_le_one'
added theorem zero_le_one
added theorem zero_le_three
added theorem zero_le_two
deleted theorem one_le_two'
deleted theorem one_le_two
deleted theorem zero_le_four
deleted theorem zero_le_one'
deleted theorem zero_le_one
deleted theorem zero_le_three
deleted theorem zero_le_two