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(Algebra/Group/InjSurj): port file #707

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat(Algebra/Group/InjSurj): port file #707

wants to merge 16 commits into from

Conversation

j-loreaux
Copy link
Collaborator

mathlib3 SHA: f69e8f317a18ab43f12cdcacaa1a3765eb512065

This was a very straightforward port.

@j-loreaux j-loreaux added awaiting-review mathlib-port This is a port of a theory file from mathlib. labels Nov 24, 2022
@j-loreaux j-loreaux changed the title raw mathport: f69e8f317a18ab43f12cdcacaa1a3765eb512065 feat(Algebra/Group/InjSurj): port file Nov 24, 2022
@dwarn
Copy link
Collaborator

dwarn commented Nov 24, 2022

Looks good to me!

@semorrison
Copy link
Contributor

bors merge

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 24, 2022
bors bot pushed a commit that referenced this pull request Nov 24, 2022
@j-loreaux @dwarn
feat(Algebra/Group/InjSurj): port file (#707)
da81e80 
mathlib3 SHA: f69e8f317a18ab43f12cdcacaa1a3765eb512065

This was a very straightforward port.

Co-authored-by: David Wärn <codwarn@gmail.com>
@bors
Copy link

bors bot commented Nov 24, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 24, 2022
@j-loreaux @dwarn
feat(Algebra/Group/InjSurj): port file (#707)
604e09a 
mathlib3 SHA: f69e8f317a18ab43f12cdcacaa1a3765eb512065

This was a very straightforward port.

Co-authored-by: David Wärn <codwarn@gmail.com>
@bors
Copy link

bors bot commented Nov 24, 2022

Build failed:

  • Build

@Ruben-VandeVelde
Copy link
Collaborator 

error: stdout:
./././Mathlib/Algebra/Group/InjSurj.lean:173:13: error: (kernel) unknown constant 'AddCancelCommMonoid.toCommMonoid'
Building Mathlib.Data.Fin.Basic
./././Mathlib/Algebra/Group/InjSurj.lean:180:49: error: Declaration Function.Injective.addCancelCommMonoid not found.

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge This PR has been sent to bors. labels Nov 24, 2022
@semorrison
Copy link
Contributor

bors d+

@bors
Copy link

bors bot commented Nov 24, 2022

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

@fpvandoorn
Copy link
Member

fpvandoorn commented Nov 24, 2022 •
edited
Loading

What's going on here: @[to_additive] doesn't automatically translate projections to extended structures other than the first, in case that the extended structures have a field in common.

The work-around is to add

attribute [to_additive AddCancelCommMonoid.toAddCommMonoid] CancelCommMonoid.toCommMonoid

after the line with class CancelCommMonoid in Group/Defs.

Remark: this can be fixed in @[to_additive] after leanprover/lean4#1881 is implemented.

@dwarn dwarn mentioned this pull request Nov 24, 2022
Closed
@j-loreaux j-loreaux added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 24, 2022
@fpvandoorn fpvandoorn mentioned this pull request Nov 24, 2022
Closed
bors bot pushed a commit that referenced this pull request Nov 24, 2022
@fpvandoorn
fix: minor changes in Groups/Defs (#719)
c174706 
* Remove instance and add `to_additive`
* Point some comments to the right issue
* Resolves the issue in #707
* Might conflict with #717
@semorrison
Copy link
Contributor

bors merge

bors bot pushed a commit that referenced this pull request Nov 24, 2022
@j-loreaux @dwarn
feat(Algebra/Group/InjSurj): port file (#707)
b711a3b 
mathlib3 SHA: f69e8f317a18ab43f12cdcacaa1a3765eb512065

This was a very straightforward port.

Co-authored-by: David Wärn <codwarn@gmail.com>
@github-actions github-actions bot mentioned this pull request Nov 24, 2022
Closed
@bors
Copy link

bors bot commented Nov 24, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(Algebra/Group/InjSurj): port file [Merged by Bors] - feat(Algebra/Group/InjSurj): port file Nov 24, 2022
@bors bors bot closed this Nov 24, 2022
@bors bors bot deleted the j-loreaux/algebra.group.inj_surj branch November 24, 2022 18:59
bors bot pushed a commit to leanprover-community/mathlib 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/mathlib 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
bors bot pushed a commit that referenced this pull request Nov 26, 2022
@dwarn @Ruben-VandeVelde
feat: port algebra.group.semiconj (#717)
0d2f062 
mathlib SHA e50b8c261b0a000b806ec0e1356b41945eda61f7

This completes an earlier partial port of the file.

~~I added a workaround for the issue explained by Floris at #707 (comment)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
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.

None yet
5 participants
@j-loreaux @dwarn @semorrison @Ruben-VandeVelde @fpvandoorn