Commit 2022-12-06 04:12 428acaae
View on Github →move(algebra/order/monoid/*): relocate zero_le_one_class
again (#17820)
#17646 move zero_le_one_class
to algebra.order.monoid.with_zero
. This PR split things about zero_le_one_class
into two files.
Also, all lemmas about numerics other than 0 and 1 require typeclass add_monoid_with_one
now.
Zulip