-
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] - feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs #5301
Conversation
… into monoid_homs
Shall we close this PR since the alternative got merged? |
I think I've found that actually this version was the better choice, as it made expressing |
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
… eric-wieser/perm-homs
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.
Thanks!
bors r+
…ype.card` theorems
e0b71ef
to
fe9d21d
Compare
Canceled. |
|
||
instance sigma_congr_right_subgroup.decidable_mem {α : Type*} {β : α → Type*} |
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.
This lemma isn't needed any more now that we have monoid_hom.decidable_mem_range
Looks like our streams crossed there - I just pushed a golf that I missed. |
I saw "eric-wieser added the awaiting-review label 6 minutes ago" and thought you were ready. Let me know when you're done, and we can get it merged. |
I'm done - I realized after double checking that I had forgotten to push one of my files. |
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.
bors r+
… into monoid_homs (#5301) This makes the corresponding subgroups available as `monoid_hom.range`. As a result, the old subgroup definitions can be removed. This also adds injectivity and cardinality lemmas.
Pull request successfully merged into master. Build succeeded: |
This makes the corresponding subgroups available as
monoid_hom.range
.As a result, the old subgroup definitions can be removed.
This also adds injectivity and cardinality lemmas.
This PR is
an alternative toa replacement for #5279