-
Notifications
You must be signed in to change notification settings - Fork 299
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] - feat(algebra/group/defs): ext lemmas for (semi)groups and monoids #8391
Conversation
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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.
@eric-wieser I was able to use your injective
strategy throughout, except around div_inv_monoid
and group
; if you wouldn't mind taking a look, I'd be grateful. Following your suggestion I changed all the ext
lemmas stated explicitly here to use {{
brackets, but note that some of the new ext
lemmas are generated by the ext
attribute.
bors d+ |
✌️ bryangingechen can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks to Eric and Chris for the review and suggestions! |
) [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236476.20boolean_algebra.2Eto_boolean_ring/near/242118386) Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Pull request successfully merged into master. Build succeeded: |
Zulip discussion
Co-authored-by: Kevin Buzzard k.buzzard@imperial.ac.uk
As you can see, this PR is very repetitive; are there some improvements to the
ext
attribute or some other automation we can use here?