-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(algebra/order/monoid): split into smaller files #16861
Conversation
This PR/issue depends on: |
…gebra_order_monoid
…gebra_order_monoid
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
With this sort of change it's useful to use leancrawler
to check that nothing really changed (e.g., like https://gist.github.com/ocfnash/4de274664fd7f0e605050d06abe0a57f).
However in this case I'm confident enough because so much depends on this and CI has passed. I spotted one typo but otherwise this LGTM.
bors d+
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <github@olivernash.org>
…anprover-community/mathlib into semorrison/split_algebra_order_monoid
bors merge |
This, along later PRs for `algebra.order.group` and `algebra.order.ring`, will replace #16792. - [x] depends on: #16172 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
- [x] depends on: #16861 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
This, along later PRs for
algebra.order.group
andalgebra.order.ring
, will replace #16792.