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 Data.Int.Cast.Lemmas #995

Closed

semorrison wants to merge 8 commits into master from data_int_cast_lemmas

Contributor

semorrison commented Dec 14, 2022

fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

semorrison added 2 commits

December 14, 2022 11:53


          feat: port Data.Int.Cast.Lemmas

d805a58


          import

47f7873

semorrison added help-wanted mathlib-port merge-conflict labels


          merge

7b2dc63

semorrison removed the merge-conflict label

semorrison added 5 commits

December 14, 2022 21:22


          fix proofs

bb828a2


          remove old ad-hoc ported file

1aea8a7

fix

055289e


          lint

9f5e133


          cleanup

688c2a1

Contributor Author

semorrison commented Dec 14, 2022

bors merge

github-actions bot added the ready-to-merge label

bors bot pushed a commit that referenced this pull request


          feat: port Data.Int.Cast.Lemmas (#995)

5c6a9da

fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

semorrison removed the help-wanted label

bors bot commented Dec 14, 2022

Pull request successfully merged into master.

Build succeeded:

bors bot changed the title ~~feat: port Data.Int.Cast.Lemmas~~ [Merged by Bors] - feat: port Data.Int.Cast.Lemmas

bors bot closed this

bors bot deleted the data_int_cast_lemmas branch

December 14, 2022 12:46

github-actions bot mentioned this pull request

[Merged by Bors] - chore(*): add mathlib4 synchronization comments leanprover-community/mathlib#17943

Closed

bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request


          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