Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(group_theory/perm/*): Generating S_n #7211

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(group_theory/perm/*): Generating S_n #7211

wants to merge 12 commits into from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Apr 15, 2021

This PR proves several lemmas about generating S_n, culminating in the following result:
If H is a subgroup of S_p, and if H has cardinality divisible by p, and if H contains a transposition, then H is all of S_p.

Open in Gitpod

@tb65536 tb65536 added the awaiting-review The author would like community review of the PR label Apr 15, 2021
@tb65536 @eric-wieser
Update src/group_theory/perm/cycle_type.lean
7653ce3 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
awainverse
awainverse reviewed Apr 15, 2021
View reviewed changes
src/group_theory/perm/cycle_type.lean Outdated Show resolved Hide resolved
src/group_theory/perm/cycles.lean Outdated Show resolved Hide resolved
@tb65536
Copy link
Collaborator Author

tb65536 commented Apr 16, 2021

Dot notation wouldn't work for that, because swap isn't a type, unlike is_swap which is

Right. I agree that this lemma should be is_swap.is_cycle. It then just seems weird to me to call the preceding lemma is_cycle.swap. Would swap_is_cycle or is_cycle_of_swap make more sense?

@eric-wieser
Copy link
Member

is_cycle_swap is probably the name I'd pick - the existing dot in the name is indeed confusing

@tb65536 @eric-wieser
Update src/group_theory/perm/cycles.lean
2277018 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jcommelin
jcommelin approved these changes Apr 20, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, but I would love to see mention of these results in module docs.

src/group_theory/perm/cycles.lean Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 20, 2021
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 20, 2021
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 21, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 21, 2021
@tb65536 tb65536 added awaiting-review The author would like community review of the PR ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 21, 2021
@robertylewis
Copy link
Member

@tb65536 For future reference: please don't add the ready-to-merge label manually. It's the bors merge comment that puts the PR on the queue, and the label gets added automatically!

bors merge

@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label Apr 22, 2021
@tb65536
Copy link
Collaborator Author

tb65536 commented Apr 22, 2021

@robertylewis Ah, thanks for clarifying this. Is there a good label for "this just need a "bors merge"", or should I just follow-up on Github or Zulip?

bors bot pushed a commit that referenced this pull request Apr 22, 2021
@tb65536
feat(group_theory/perm/*): Generating S_n (#7211)
1585b14 
This PR proves several lemmas about generating S_n, culminating in the following result:
If H is a subgroup of S_p, and if H has cardinality divisible by p, and if H contains a transposition, then H is all of S_p.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
@robertylewis
Copy link
Member

Probably best to mark it awaiting-review and ping whoever approved it before.

@bors
Copy link

bors bot commented Apr 23, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(group_theory/perm/*): Generating S_n [Merged by Bors] - feat(group_theory/perm/*): Generating S_n Apr 23, 2021
@bors bors bot closed this Apr 23, 2021
@bors bors bot deleted the generating_Sn branch April 23, 2021 00:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin approved these changes

@awainverse awainverse awainverse left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@tb65536 @eric-wieser @jcommelin @robertylewis @awainverse