-
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(group_theory/perm/{cycles, cycle_type}): permutations are conjugate iff they have the same cycle type #7335
Conversation
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Co-authored-by: tb65536 <tb65536@users.noreply.github.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.
LGTM, but I haven't touched this part of the library, so I'm hesitant to hit merge.
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 merge
…ate iff they have the same cycle type (#7335) Slightly strengthens the induction principle `equiv.perm.cycle_induction_on` Proves that two permutations are conjugate iff they have the same cycle type: `equiv.perm.is_conj_iff_cycle_type_eq` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Thomas Browning <tb65536@uw.edu>
Build failed (retrying...): |
I believe the new simp lemmas conflict with something in this failure bors r- |
Canceled. |
Hopefully that fixes everything... |
The problem seems fixed, shall we try again? |
bors merge |
bors crashed |
…ate iff they have the same cycle type (#7335) Slightly strengthens the induction principle `equiv.perm.cycle_induction_on` Proves that two permutations are conjugate iff they have the same cycle type: `equiv.perm.is_conj_iff_cycle_type_eq` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Thomas Browning <tb65536@uw.edu>
Pull request successfully merged into master. Build succeeded: |
Slightly strengthens the induction principle
equiv.perm.cycle_induction_on
Proves that two permutations are conjugate iff they have the same cycle type:
equiv.perm.is_conj_iff_cycle_type_eq