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/p_group): Groups of order p^2 are commutative #8632

Closed
wants to merge 56 commits into from
Closed

[Merged by Bors] - feat(group_theory/p_group): Groups of order p^2 are commutative #8632

wants to merge 56 commits into from

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 commented Aug 11, 2021 •
edited

I also made a p_group namespace and moved some lemmas about actions of p-groups out of the mul_action namespace and into the p_group namespace.

Open in Gitpod

@github-actions github-actions bot added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Aug 11, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 12, 2021
@ChrisHughes24 @eric-wieser
Update src/group_theory/group_action/conj.lean
6be95c6 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ChrisHughes24 ChrisHughes24 added the awaiting-review The author would like community review of the PR label Aug 12, 2021
@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 Jul 16, 2022
@erdOne erdOne mentioned this pull request Jul 17, 2022
Closed
kckennylau and others added 2 commits July 20, 2022 03:39
@kckennylau @tb65536 @eric-wieser
Apply suggestions from code review
cd6e15f 
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@kckennylau
fix errors and style
f0d2687
@kckennylau @tb65536
Update src/group_theory/p_group.lean
2e74628 
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
@kckennylau kckennylau added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 21, 2022
@jcommelin
Copy link
Member

@eric-wieser Are you happy with how the instances work out?

Otherwise: LGTM. If you agree, please send it to bors.

eric-wieser
eric-wieser approved these changes Jul 29, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Otherwise LGTM. The comm_group_of_card_eq_prime_sq def is a bit of a foot-gun as described in #14960 (comment); but it's no worse than the other foot-guns it's built out of, and cleaning them all up at once later makes more sense anyway.

@eric-wieser
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Jul 29, 2022

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 29, 2022
@kckennylau @eric-wieser
Update src/group_theory/p_group.lean
2d7a124 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@ChrisHughes24
Copy link
Member Author

Bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 30, 2022
bors bot pushed a commit that referenced this pull request Jul 30, 2022
@ChrisHughes24
feat(group_theory/p_group): Groups of order p^2 are commutative (#8632)
09afe57 
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
@bors
Copy link

bors bot commented Jul 30, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(group_theory/p_group): Groups of order p^2 are commutative [Merged by Bors] - feat(group_theory/p_group): Groups of order p^2 are commutative Jul 30, 2022
@bors bors bot closed this Jul 30, 2022
@bors bors bot deleted the p2-comm branch July 30, 2022 01:38
bottine pushed a commit to bottine/mathlib that referenced this pull request Jul 30, 2022
@ChrisHughes24 @bottine
feat(group_theory/p_group): Groups of order p^2 are commutative (lean…
7c6abc1 
…prover-community#8632)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
robertylewis pushed a commit that referenced this pull request Aug 2, 2022
@ChrisHughes24 @robertylewis
feat(group_theory/p_group): Groups of order p^2 are commutative (#8632)
d529451 
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
khwilson pushed a commit that referenced this pull request Aug 2, 2022
@ChrisHughes24 @khwilson
feat(group_theory/p_group): Groups of order p^2 are commutative (#8632)
92a35a3 
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@tb65536 tb65536 tb65536 left review comments

@kckennylau kckennylau kckennylau left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees

@eric-wieser eric-wieser

Labels
delegated The PR author may merge after reviewing final suggestions. 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
7 participants
@ChrisHughes24 @alexjbest @jcommelin @eric-wieser @tb65536 @kckennylau @Ruben-VandeVelde