mathlib

49f5a159 - feat(algebra/ordered_ring): more granular typeclasses for `with_top α` and `with_bot α` (#7845)

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