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: Prove isomorphism implies equality of normal closure subgroups #9185

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat: Prove isomorphism implies equality of normal closure subgroups #9185

wants to merge 10 commits into from

Conversation

newell
Copy link
Collaborator

@newell newell commented Dec 21, 2023 •
edited

feat: Prove isomorphism implies equality of normal closure subgroups

Co-authored-by: Riccardo Brasca riccardo.brasca@gmail.com

Open in Gitpod

@newell @eric-wieser
Update Mathlib/GroupTheory/Subgroup/Basic.lean
b03120c 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@newell newell added the awaiting-review The author would like community review of the PR label Dec 26, 2023
@tb65536
Copy link
Collaborator

tb65536 commented Jan 1, 2024

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 1, 2024

🚀 Pull request has been placed on the maintainer queue by tb65536.

jcommelin
jcommelin approved these changes Jan 2, 2024
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.

Thanks 🎉

bors merge

(Future TODO: someone should clean up the variable names. G and N are playing mostly symmetric roles, but their names don't suggest that.)

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 2, 2024
@newell @eric-wieser
feat: Prove isomorphism implies equality of normal closure subgroups (#…
a4e04c2 
…9185)

feat: Prove isomorphism implies equality of normal closure subgroups

Co-authored-by: Riccardo Brasca riccardo.brasca@gmail.com



Co-authored-by: Newell Jensen <newell@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 2, 2024

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

@mathlib-bors mathlib-bors bot changed the title feat: Prove isomorphism implies equality of normal closure subgroups [Merged by Bors] - feat: Prove isomorphism implies equality of normal closure subgroups Jan 2, 2024
@mathlib-bors mathlib-bors bot closed this Jan 2, 2024
@mathlib-bors mathlib-bors bot deleted the newell/normal-closure-equiv-map branch January 2, 2024 08:28
@newell newell mentioned this pull request Jan 17, 2024
Closed
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

@alreadydone alreadydone alreadydone left review comments

@tb65536 tb65536 tb65536 left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

@github-actions github-actions[bot] github-actions left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@newell @tb65536 @eric-wieser @alreadydone @jcommelin @riccardobrasca @leanprover-community-mathlib4-bot