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: Data.Int.Order.Basic #938

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat port: Data.Int.Order.Basic #938

wants to merge 19 commits into from

Conversation

ChrisHughes24
Copy link
Member

10b4e499f43088dd3bb7b5796184ad5216648ab1

@ChrisHughes24 ChrisHughes24 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 9, 2022
@Ruben-VandeVelde
Copy link
Collaborator

I'm running into a lot of trouble with div/mod here - it seems like those changed behaviour in lean4.

@ChrisHughes24
Copy link
Member Author

I remember the definition of mod changed. Probably just make a PR to Lean4 correcting the definition

@ChrisHughes24
Copy link
Member Author

Zulip discussion about some coercion issues here

@semorrison
Copy link
Contributor

We may be able to proceed here by merging #972 into this PR.

@semorrison
Copy link
Contributor

semorrison commented Dec 13, 2022 •
edited

And #973 will give us mathlib3 compatible Div Int and Mod Int instances. (Now merged into this via master.)

@ChrisHughes24
Copy link
Member Author

Most of this file is about div and mod and the lemma names clash with the different definition of div and mod in Std. Should we change the name of Int.div and the lemmas about it?

@digama0
Copy link
Member

digama0 commented Dec 13, 2022

The std convention is to rename all the lemmas to use ediv instead of div, even though it is written with the / notation now. I think we should keep doing this until a PR to change the names goes through.

@semorrison semorrison added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 13, 2022
@semorrison semorrison mentioned this pull request Dec 13, 2022
Open
@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 13, 2022
bors bot pushed a commit that referenced this pull request Dec 13, 2022
@ChrisHughes24 @Ruben-VandeVelde @semorrison
feat port: Data.Int.Order.Basic (#938)
6a7ba1d 
10b4e499f43088dd3bb7b5796184ad5216648ab1

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Dec 13, 2022

Canceled.

@semorrison
Copy link
Contributor

bors merge

bors bot pushed a commit that referenced this pull request Dec 13, 2022
@ChrisHughes24 @Ruben-VandeVelde @semorrison
feat port: Data.Int.Order.Basic (#938)
eab8de7 
10b4e499f43088dd3bb7b5796184ad5216648ab1

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Dec 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat port: Data.Int.Order.Basic [Merged by Bors] - feat port: Data.Int.Order.Basic Dec 13, 2022
@bors bors bot closed this Dec 13, 2022
@bors bors bot deleted the Data.Int.Order.Basic branch December 13, 2022 23:46
@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
No reviews
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
@ChrisHughes24 @Ruben-VandeVelde @semorrison @digama0