Skip to content

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

Closed
riccardobrasca wants to merge 15 commits intomasterfrom
RB/EckmannHilton
Closed

[Merged by Bors] - feat: port Algebra.GroupTheory.EckmannHilton#626
riccardobrasca wants to merge 15 commits intomasterfrom
RB/EckmannHilton

Conversation

@riccardobrasca
Copy link
Copy Markdown
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 commented Nov 17, 2022
View reviewed changes
riccardobrasca
riccardobrasca commented Nov 17, 2022
View reviewed changes
@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
Copy Markdown
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
pechersky
pechersky reviewed Nov 22, 2022
View reviewed changes
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Nov 22, 2022
View reviewed changes
@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
riccardobrasca and others added 2 commits November 22, 2022 15:45
@riccardobrasca @Ruben-VandeVelde
Update Mathlib/GroupTheory/EckmannHilton.lean
0fc5566 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@riccardobrasca
Merge remote-tracking branch 'origin/master' into RB/EckmannHilton
355836d
@kim-em
Copy link
Copy Markdown
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
Copy Markdown
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 <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

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
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
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
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