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.Order.Hom.Monoid #944

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Order.Hom.Monoid #944

wants to merge 13 commits into from

Conversation

dupuisf
Copy link
Contributor

@dupuisf dupuisf commented Dec 10, 2022 •
edited by github-actions bot

mathlib3 SHA: 3342d1b2178381196f818146ff79bc0e7ccd9e2d

@dupuisf dupuisf added help-wanted The author needs attention to resolve issues WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 10, 2022
@kbuzzard
Copy link
Member

kbuzzard commented Dec 10, 2022 •
edited

Right now porting this file seems to be blocked on leanprover/lean4#1940 (in the sense that a lot of instances will need to be synthesized by hand because typeclass inference is timing out). Zulip discussion here.

@kbuzzard
Copy link
Member

Gabriel has explained the fix and it works in our use case.

@fpvandoorn fpvandoorn mentioned this pull request Dec 11, 2022
Closed
@dupuisf dupuisf added blocked-by-other-PR This PR depends on another PR which is still in the queue. and removed help-wanted The author needs attention to resolve issues labels Dec 11, 2022
bors bot pushed a commit that referenced this pull request Dec 12, 2022
@fpvandoorn
fix: to_additive now translates projections (#952)
ce3c4a8 
* Projections can occur in terms that use the structure notation `{ ... with ... }`.
* Nobody submitted a MWE, so I didn't add a test (I don't know exactly how to ensure that a projection is included in a term). I did check that this fixes the issues in #944 and #912
* Closes #939, it fixes both comments mentioned there.
@semorrison semorrison removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Dec 12, 2022
@semorrison
Copy link
Contributor

This PR/issue depends on:

@dupuisf dupuisf added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 13, 2022
@dupuisf
Copy link
Contributor Author

dupuisf commented Dec 13, 2022

This is now ready for review. Note that I removed a few @[simp] tags that (according to the linter) are now superfluous due to the way coercions are handled in Lean 4.

@semorrison semorrison 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 Dec 13, 2022
dupuisf and others added 4 commits December 13, 2022 16:35
@dupuisf @semorrison
Update Mathlib/Algebra/Order/Hom/Monoid.lean
9b2064c 
Co-authored-by: Scott Morrison <scott@tqft.net>
@dupuisf @semorrison
Update Mathlib/Algebra/Order/Hom/Monoid.lean
909c9fb 
Co-authored-by: Scott Morrison <scott@tqft.net>
@dupuisf @semorrison
Update Mathlib/Algebra/Order/Hom/Monoid.lean
2ef49cb 
Co-authored-by: Scott Morrison <scott@tqft.net>
@dupuisf
alignment tags for additive versions
93ed535
@dupuisf dupuisf 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 Dec 13, 2022
@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions 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 Dec 14, 2022
bors bot pushed a commit that referenced this pull request Dec 14, 2022
@dupuisf @kbuzzard @semorrison
feat: port Algebra.Order.Hom.Monoid (#944)
098452b 
mathlib3 SHA: 3342d1b2178381196f818146ff79bc0e7ccd9e2d

- [x] depends on: #952 

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
@bors
Copy link

bors bot commented Dec 14, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Algebra.Order.Hom.Monoid [Merged by Bors] - feat: port Algebra.Order.Hom.Monoid Dec 14, 2022
@bors bors bot closed this Dec 14, 2022
@bors bors bot deleted the dupuisf/algebra/order/hom/monoid branch December 14, 2022 02:02
@github-actions github-actions bot mentioned this pull request Dec 14, 2022
Closed
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Dec 15, 2022
@leanprover-community-bot @j-loreaux
chore(*): add mathlib4 synchronization comments (#17943)
a59dad5 
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.euclidean_domain.basic`: leanprover-community/mathlib4#919
* `algebra.field.basic`: leanprover-community/mathlib4#975
* `algebra.group.opposite`: leanprover-community/mathlib4#912
* `algebra.group.prod`: leanprover-community/mathlib4#968
* `algebra.group.with_one.units`: leanprover-community/mathlib4#955
* `algebra.group_power.ring`: leanprover-community/mathlib4#979
* `algebra.hom.equiv.type_tags`: leanprover-community/mathlib4#943
* `algebra.hom.ring`: leanprover-community/mathlib4#958
* `algebra.invertible`: leanprover-community/mathlib4#930
* `algebra.order.field.canonical.basic`: leanprover-community/mathlib4#1018
* `algebra.order.field.canonical.defs`: leanprover-community/mathlib4#985
* `algebra.order.field.inj_surj`: leanprover-community/mathlib4#1017
* `algebra.order.group.densely_ordered`: leanprover-community/mathlib4#956
* `algebra.order.group.min_max`: leanprover-community/mathlib4#933
* `algebra.order.group.prod`: leanprover-community/mathlib4#1026
* `algebra.order.group.with_top`: leanprover-community/mathlib4#946
* `algebra.order.hom.monoid`: leanprover-community/mathlib4#944
* `algebra.order.monoid.prod`: leanprover-community/mathlib4#987
* `algebra.order.monoid.to_mul_bot`: leanprover-community/mathlib4#1024
* `algebra.order.ring.abs`: leanprover-community/mathlib4#929
* `algebra.order.ring.cone`: leanprover-community/mathlib4#935
* `algebra.order.sub.basic`: leanprover-community/mathlib4#936
* `algebra.order.sub.with_top`: leanprover-community/mathlib4#932
* `algebra.order.with_zero`: leanprover-community/mathlib4#903
* `combinatorics.quiver.arborescence`: leanprover-community/mathlib4#997
* `combinatorics.quiver.cast`: leanprover-community/mathlib4#990
* `control.traversable.lemmas`: leanprover-community/mathlib4#948
* `data.bool.set`: leanprover-community/mathlib4#960
* `data.int.cast.field`: leanprover-community/mathlib4#1016
* `data.int.cast.lemmas`: leanprover-community/mathlib4#995
* `data.int.cast.prod`: leanprover-community/mathlib4#1015
* `data.int.div`: leanprover-community/mathlib4#1011
* `data.int.dvd.basic`: leanprover-community/mathlib4#996
* `data.int.order.basic`: leanprover-community/mathlib4#938
* `data.nat.cast.basic`: leanprover-community/mathlib4#980
* `data.nat.cast.prod`: leanprover-community/mathlib4#1010
* `data.nat.cast.with_top`: leanprover-community/mathlib4#1019
* `data.nat.gcd.basic`: leanprover-community/mathlib4#965
* `data.nat.order.basic`: leanprover-community/mathlib4#907
* `data.nat.order.lemmas`: leanprover-community/mathlib4#927
* `data.nat.set`: leanprover-community/mathlib4#961
* `data.nat.upto`: leanprover-community/mathlib4#1020
* `data.pequiv`: leanprover-community/mathlib4#1008
* `data.set.basic`: leanprover-community/mathlib4#892
* `data.set.bool_indicator`: leanprover-community/mathlib4#988
* `data.set.image`: leanprover-community/mathlib4#949
* `data.set.n_ary`: leanprover-community/mathlib4#969
* `data.set.opposite`: leanprover-community/mathlib4#983
* `data.set.prod`: leanprover-community/mathlib4#1004
* `data.set.sigma`: leanprover-community/mathlib4#982
* `data.set_like.basic`: leanprover-community/mathlib4#993
* `data.two_pointing`: leanprover-community/mathlib4#984
* `logic.embedding.set`: leanprover-community/mathlib4#986
* `logic.equiv.embedding`: leanprover-community/mathlib4#1021
* `order.directed`: leanprover-community/mathlib4#963
* `order.rel_iso.set`: leanprover-community/mathlib4#1005
* `order.well_founded`: leanprover-community/mathlib4#970
* `ring_theory.coprime.basic`: leanprover-community/mathlib4#899



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. 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
4 participants
@dupuisf @kbuzzard @semorrison @Ruben-VandeVelde