Skip to content

feat: parity between Int.ediv/tdiv/fdiv theorems#7358

Merged
kim-em merged 11 commits intomasterfrom
tmod_fmod2
Mar 6, 2025
Merged

feat: parity between Int.ediv/tdiv/fdiv theorems#7358
kim-em merged 11 commits intomasterfrom
tmod_fmod2

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Mar 6, 2025

This PR fills further gaps in the integer division API, and mostly achieves parity between the three variants of integer division. There are still some inequality lemmas about tdiv and fdiv that are missing, but as they would have quite awkward statements I'm hoping that for now no one is going to miss them.

@kim-em kim-em added the changelog-library Library label Mar 6, 2025
@kim-em kim-em added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Mar 6, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 05:15 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 6, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
Update lean-toolchain for testing leanprover/lean4#7358
35f2705
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
Update lean-toolchain for testing leanprover/lean4#7358
6ca4705
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 6, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 6, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 6, 2025 11:49 Inactive
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@kim-em
fixes for leanprover/lean4#7358
2da3cda
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@kim-em
fixes for leanprover/lean4#7358
76d0e07
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
@kim-em
fixes for leanprover/lean4#7358
de1559a
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Mar 6, 2025

Builds Mathlib locally after a few changes, so I'll enqueue this.

@kim-em kim-em enabled auto-merge March 6, 2025 12:00
@kim-em kim-em added this pull request to the merge queue Mar 6, 2025
@kim-em kim-em removed awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 6, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2025
Trigger CI for leanprover/lean4#7358
95f90d8
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 6, 2025
Trigger CI for leanprover/lean4#7358
5cc9152
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 6, 2025
Merged via the queue into master with commit c5cec10 Mar 6, 2025
21 checks passed
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025
@jcommelin @kim-em
@TwoFX @nomeata @kmill @tydeu @jrr6 @kbuzzard @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-09 (#22758)
ec93745 
* chore: adaptations for nightly-2025-02-20

* Merge master into nightly-testing

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

* chore: adaptations for nightly-2025-02-20 (#22144)

* lake update

* fixes

* fix namespace

* fix test

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-06

* copy test from master

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-07

* chore: bump to nightly-2025-02-08

* update

* chore: bump to nightly-2025-02-09

* didn't commit

* fix

* fix test

* Update lean-toolchain for testing leanprover/lean4#7013

* chore: bump to nightly-2025-02-10

* fixes for leanprover/lean4#7013

* fixes for leanprover/lean4#7013

* Trigger CI for leanprover/lean4#7013

* chore: bump to nightly-2025-02-11

* update

* Update lean-toolchain for testing leanprover/lean4#7046

* Trigger CI for leanprover/lean4#7046

* Switch from mk to ofBitVec

* chore: bump to nightly-2025-02-12

* Update lean-toolchain for testing leanprover/lean4#7050

* lake update

* lake update

* fixes

* another maxheartbeats

* fix tests

* Update lean-toolchain for testing leanprover/lean4#7059

* fix

* chore: bump to nightly-2025-02-13

* lake update

* fixes

* lake exe shake --fix

* Update lean-toolchain for testing leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

* chore: adaptations for nightly-2025-02-13

* remove upstreamed

* Trigger CI for leanprover/lean4#7059

* Trigger CI for leanprover/lean4#7059

* chore: bump to nightly-2025-02-14

* Trigger CI for leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

* Update lean-toolchain for testing leanprover/lean4#7082

* quite a bit more to go

* lake update

* fix merge

* fix

* adapt

* adapt

* Trigger CI for leanprover/lean4#7082

* Trigger CI for leanprover/lean4#7069

* lake update

* lake update

* fixes

* fixes

* chore: bump to nightly-2025-02-15

* Trigger CI for leanprover/lean4#7069

* Update lean-toolchain for testing leanprover/lean4#7100

* chore: bump to nightly-2025-02-16

* fixes

* fixes 2

* fixes 3

* built mathlib

* Trigger CI for leanprover/lean4#7069

* fix simps test

* fixes for leanprover/lean4#7059

* fix: cache lib dir (adaption for lean4#7001) (#21967)

* fixes

* fixes for leanprover/lean4#7059

* restore broken files

* chore: bump to nightly-2025-02-17

* lake update

* lake update

* oops

* comment out broken files

* longFile

* oops, one more

* .

* searchPath

* .

* Update lean-toolchain for testing leanprover/lean4#7103

* fixes

* update manifest

* fix

* fix

* Trigger CI for leanprover/lean4#7103

* chore: bump to nightly-2025-02-18

* lake update

* deprecations

* restore computability files broken by defeq yesterday

* fixes

* chore: adaptations for nightly-2025-02-18

* chore: bump to nightly-2025-02-19

* lake update

* fixes

* fix merge

* chore: adaptations for nightly-2025-02-19

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-20

* fix merge

* chore: adaptations for nightly-2025-02-20

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>

* chore: bump to nightly-2025-02-21

* chore: bump to nightly-2025-02-22

* chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation

* Update lean-toolchain for testing leanprover/lean4#7196

* fixes

* update batteries

* update proofwidgets

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-02-24

* lake update

* fixes

* deprecations

* .

* archive

* fix tests

* fix tests

* chore: adaptations for nightly-2025-02-24 (#22266)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

* chore: bump to nightly-2025-02-25

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Adapt

* Trigger CI for leanprover/lean4#7166

* revert Mathlib/Data/Multiset/Basic, and refix

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-26

* remove upstreamed

* fix

* fix tests

* Apply suggestions from code review

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* chore: adaptations for nightly-2025-02-26 (#22347)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

* chore: bump to nightly-2025-02-27

* Trigger CI for leanprover/lean4#7166

* Update lean-toolchain for testing leanprover/lean4#7259

* fix

* I would not have guessed that this lemma already exists!

* chore: bump to nightly-2025-02-28

* fix

* chore: bump to nightly-2025-03-01

* chore: bump to nightly-2025-03-02

* Merge master into nightly-testing

* deprecation

* Trigger CI for leanprover/lean4#7166

* deprecation

* chore: adaptations for nightly-2025-03-02 (#22460)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2025-03-02

* chore: bump to nightly-2025-03-03

* remove upstreamed

* chore: adaptations for nightly-2025-03-03

* Trigger CI for leanprover/lean4#7166

* chore: adaptations for nightly-2025-03-03 (#22493)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

* bump toolchain and dependencies

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-03-04

* lake update

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-03-05

* fix?

* add adaptation notes to revert _root_

* Update lean-toolchain for testing leanprover/lean4#7358

* chore: bump to nightly-2025-03-06

* chore: adaptations for nightly-2025-03-06

* chore: adaptations for nightly-2025-03-06

* Merge master into nightly-testing

* chore: bump to nightly-2025-03-06

* Update lean-toolchain for testing leanprover/lean4#7261

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7261

* fix Mathlib.Linter.getNamesFrom

* chore: adaptations for nightly-2025-03-06

* chore: bump to nightly-2025-03-07

* lake update

* add_div is protected

* Update lean-toolchain for testing leanprover/lean4#7378

* More like that

* adapt

* Trigger CI for leanprover/lean4#7378

* Fix

* fix

* chore: bump to nightly-2025-03-08

* lake update

* chore: bump to nightly-2025-03-09

* chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215

* process adaptation notes

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 12, 2025
@jcommelin @jrr6
@kmill @kim-em @nomeata @kbuzzard @TwoFX @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-11 (#22826)
2677da0 
* chore: bump to nightly-2025-02-21

* chore: bump to nightly-2025-02-22

* chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation

* Update lean-toolchain for testing leanprover/lean4#7196

* fixes

* update batteries

* update proofwidgets

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-02-24

* lake update

* fixes

* deprecations

* .

* archive

* fix tests

* fix tests

* chore: adaptations for nightly-2025-02-24 (#22266)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

* chore: bump to nightly-2025-02-25

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Adapt

* Trigger CI for leanprover/lean4#7166

* revert Mathlib/Data/Multiset/Basic, and refix

* Merge master into nightly-testing

* chore: bump to nightly-2025-02-26

* remove upstreamed

* fix

* fix tests

* Apply suggestions from code review

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* chore: adaptations for nightly-2025-02-26 (#22347)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

* chore: bump to nightly-2025-02-27

* Trigger CI for leanprover/lean4#7166

* Update lean-toolchain for testing leanprover/lean4#7259

* fix

* I would not have guessed that this lemma already exists!

* chore: bump to nightly-2025-02-28

* fix

* chore: bump to nightly-2025-03-01

* chore: bump to nightly-2025-03-02

* Merge master into nightly-testing

* deprecation

* Trigger CI for leanprover/lean4#7166

* deprecation

* chore: adaptations for nightly-2025-03-02 (#22460)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

* chore: adaptations for nightly-2025-03-02

* chore: bump to nightly-2025-03-03

* remove upstreamed

* chore: adaptations for nightly-2025-03-03

* Trigger CI for leanprover/lean4#7166

* chore: adaptations for nightly-2025-03-03 (#22493)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

* bump toolchain and dependencies

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-03-04

* lake update

* Trigger CI for leanprover/lean4#7166

* chore: bump to nightly-2025-03-05

* fix?

* add adaptation notes to revert _root_

* Update lean-toolchain for testing leanprover/lean4#7358

* chore: bump to nightly-2025-03-06

* chore: adaptations for nightly-2025-03-06

* chore: adaptations for nightly-2025-03-06

* Merge master into nightly-testing

* chore: bump to nightly-2025-03-06

* Update lean-toolchain for testing leanprover/lean4#7261

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7261

* fix Mathlib.Linter.getNamesFrom

* chore: adaptations for nightly-2025-03-06

* chore: bump to nightly-2025-03-07

* lake update

* add_div is protected

* Update lean-toolchain for testing leanprover/lean4#7378

* More like that

* adapt

* Trigger CI for leanprover/lean4#7378

* Fix

* fix

* chore: bump to nightly-2025-03-08

* lake update

* chore: bump to nightly-2025-03-09

* chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215

* process adaptation notes

* chore: bump to nightly-2025-03-10

* chore: adaptations for nightly-2025-03-10

* rm upstreamed

* rm upstreamed

* chore: bump to nightly-2025-03-11

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@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

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@kim-em