Commit 2021-06-10 16:03 49f5a159

feat(algebra/ordered_ring): more granular typeclasses for with_top α and with_bot α (#7845) with_top α and with_bot α now inherit the following typeclasses from α with suitable assumptions:

• mul_zero_one_class
• semigroup_with_zero
• monoid_with_zero
• comm_monoid_with_zero These were all split out of the existing canonically_ordered_comm_semiring, with their proofs unchanged. The same instances are added for with_bot. It is not possible to split further, as distrib' requires add_eq_zero_iff, and canonically_ordered_comm_semiring is the smallest typeclass that provides both this lemma and mul_zero_class. With these instances in place, we can now show comm_monoid_with_zero ereal.