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: port Algebra.GroupTheory.EckmannHilton #626

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat: port Algebra.GroupTheory.EckmannHilton #626

wants to merge 15 commits into from

Conversation

riccardobrasca
Copy link
Member

@riccardobrasca riccardobrasca commented Nov 17, 2022 •
edited
Loading

mathlib3 sha: 71dbd401af609bb5065d060b8f221d2a31e2b8d7

@riccardobrasca riccardobrasca changed the title [Merged by Bors] - feat: port feat: port Algebra.GroupTheory.EckmannHilton Nov 17, 2022
@riccardobrasca riccardobrasca added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. and removed awaiting-review labels Nov 17, 2022
@kim-em
Copy link
Contributor

kim-em commented Nov 18, 2022

Please fix long lines, and add the import line to Mathlib.lean. Then probably good to go.

@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes and removed WIP Work in progress labels Nov 18, 2022
@riccardobrasca riccardobrasca added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 18, 2022
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Nov 22, 2022
View reviewed changes
Mathlib/GroupTheory/EckmannHilton.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/EckmannHilton.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/EckmannHilton.lean Outdated Show resolved Hide resolved
@Ruben-VandeVelde Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Nov 22, 2022
@kim-em
Copy link
Contributor

kim-em commented Nov 23, 2022

Could you click resolve on the queries, and mark back as awaiting-review, when ready? (I think, from the commit messages, that this may be the case already, but don't really want to verify.)

@riccardobrasca riccardobrasca added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 23, 2022
@kim-em
Copy link
Contributor

kim-em commented Nov 23, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 23, 2022
@riccardobrasca @kim-em
feat: port Algebra.GroupTheory.EckmannHilton (#626)
8b2d844 
mathlib3 sha: 71dbd401af609bb5065d060b8f221d2a31e2b8d7


Co-authored-by: Scott Morrison <[email protected]>
@bors
Copy link

bors bot commented Nov 23, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.GroupTheory.EckmannHilton [Merged by Bors] - feat: port Algebra.GroupTheory.EckmannHilton Nov 23, 2022
@bors bors bot closed this Nov 23, 2022
@bors bors bot deleted the RB/EckmannHilton branch November 23, 2022 19:32
@github-actions github-actions bot mentioned this pull request Nov 23, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 23, 2022
@leanprover-community-bot
chore(*): add mathlib4 synchronization comments (#17686)
1044429 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 24, 2022
@leanprover-community-bot
chore(*): add mathlib4 synchronization comments (#17686)
fe771af 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.inj_surj`: leanprover-community/mathlib4#707
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.group.units`: leanprover-community/mathlib4#549
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `data.ulift`: leanprover-community/mathlib4#703
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
bors bot pushed a commit to leanprover-community/mathlib3 that referenced this pull request Nov 25, 2022
@leanprover-community-bot
chore(*): add mathlib4 synchronization comments (#17686)
cb1d279 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.char_zero.defs`: leanprover-community/mathlib4#661
* `algebra.group.inj_surj`: leanprover-community/mathlib4#707
* `algebra.group.order_synonym`: leanprover-community/mathlib4#651
* `algebra.group.units`: leanprover-community/mathlib4#549
* `algebra.hierarchy_design`: leanprover-community/mathlib4#657
* `algebra.opposites`: leanprover-community/mathlib4#644
* `algebra.quotient`: leanprover-community/mathlib4#643
* `algebra.ring.defs`: leanprover-community/mathlib4#655
* `algebra.ring.order_synonym`: leanprover-community/mathlib4#671
* `control.equiv_functor`: leanprover-community/mathlib4#649
* `data.dlist.basic`: leanprover-community/mathlib4#616
* `data.int.cast.basic`: leanprover-community/mathlib4#670
* `data.lazy_list`: leanprover-community/mathlib4#686
* `data.list.lex`: leanprover-community/mathlib4#672
* `data.option.n_ary`: leanprover-community/mathlib4#656
* `data.sigma.lex`: leanprover-community/mathlib4#646
* `data.ulift`: leanprover-community/mathlib4#703
* `group_theory.eckmann_hilton`: leanprover-community/mathlib4#626
* `logic.equiv.basic`: leanprover-community/mathlib4#631
* `order.iterate`: leanprover-community/mathlib4#648
@github-actions github-actions bot mentioned this pull request Nov 29, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

@pechersky pechersky pechersky left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@riccardobrasca @kim-em @pechersky @Ruben-VandeVelde