Skip to content

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

Closed
dupuisf wants to merge 13 commits intomasterfrom
dupuisf/algebra/order/hom/monoid
Closed

[Merged by Bors] - feat: port Algebra.Order.Hom.Monoid#944
dupuisf wants to merge 13 commits intomasterfrom
dupuisf/algebra/order/hom/monoid

Conversation

@dupuisf
Copy link
Copy Markdown
Contributor

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

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
Copy Markdown
Member

kbuzzard commented Dec 10, 2022 •
edited
Loading

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.

@Ruben-VandeVelde Ruben-VandeVelde added the blocked-by-core-PR This PR depends on a PR to Core/Std label Dec 10, 2022
@kbuzzard kbuzzard removed the blocked-by-core-PR This PR depends on a PR to Core/Std label Dec 10, 2022
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Dec 10, 2022

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 (this label is automatically managed by a bot) 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.
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 12, 2022
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 12, 2022

This PR/issue depends on:

@dupuisf dupuisf added awaiting-review and removed WIP Work in progress labels Dec 13, 2022
@dupuisf
Copy link
Copy Markdown
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.

kim-em
kim-em reviewed Dec 13, 2022
View reviewed changes
kim-em
kim-em reviewed Dec 13, 2022
View reviewed changes
kim-em
kim-em reviewed Dec 13, 2022
View reviewed changes
kim-em
kim-em reviewed Dec 13, 2022
View reviewed changes
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Dec 13, 2022
dupuisf and others added 4 commits December 13, 2022 16:35
@dupuisf @kim-em
Update Mathlib/Algebra/Order/Hom/Monoid.lean
9b2064c 
Co-authored-by: Scott Morrison <scott@tqft.net>
@dupuisf @kim-em
Update Mathlib/Algebra/Order/Hom/Monoid.lean
909c9fb 
Co-authored-by: Scott Morrison <scott@tqft.net>
@dupuisf @kim-em
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 and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Dec 13, 2022
kim-em
kim-em reviewed Dec 14, 2022
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Dec 14, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 14, 2022
bors bot pushed a commit that referenced this pull request Dec 14, 2022
@dupuisf @kbuzzard @kim-em
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
Copy Markdown

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/mathlib3 that referenced this pull request Dec 15, 2022
@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

@kim-em kim-em kim-em 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.

4 participants

@dupuisf @kbuzzard @kim-em @Ruben-VandeVelde