Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`.
- Loading branch information
1 parent
079b8a1
commit 49f5a15
Showing
3 changed files
with
184 additions
and
47 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters