Skip to content

feat: Nat.gcd lemmas#7756

Merged
TwoFX merged 7 commits intomasterfrom
markus/nat-gcd
Apr 1, 2025
Merged

feat: Nat.gcd lemmas#7756
TwoFX merged 7 commits intomasterfrom
markus/nat-gcd

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Mar 31, 2025

This PR adds lemmas about Nat.gcd (some of which are currently present in mathlib).

@TwoFX TwoFX added the changelog-library Library label Mar 31, 2025
@TwoFX TwoFX requested a review from kim-em as a code owner March 31, 2025 14:41
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 31, 2025 14:55 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 31, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 31, 2025
Update lean-toolchain for testing leanprover/lean4#7756
f1ea7e2
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 31, 2025
Update lean-toolchain for testing leanprover/lean4#7756
81642e1
@ghost
Copy link
Copy Markdown

ghost commented Mar 31, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 31, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 1, 2025 06:12 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
9477c7d
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
34f26b7
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 1, 2025 07:34 Inactive
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 1, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
ec95531
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
c9d0983
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 1, 2025 08:15 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
e5d6851
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
5889184
@ghost ghost added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Apr 1, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 1, 2025 13:04 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
807a483
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
ecd562c
@ghost ghost removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 1, 2025
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 1, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 1, 2025 15:15 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
f741dd3
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 1, 2025
Trigger CI for leanprover/lean4#7756
9b2ff4b
@TwoFX TwoFX added this pull request to the merge queue Apr 1, 2025
Merged via the queue into master with commit b6f18e8 Apr 1, 2025
17 checks passed
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Apr 3, 2025
@kim-em @kmill
@jcommelin @TwoFX @digama0 @Kha
chore: adaptations for nightly-2025-04-02 (#23610)
11dad05 
* chore: bump to nightly-2025-03-22

* Merge master into nightly-testing

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

* fix

* Merge master into nightly-testing

* protected

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

* update batteries and aesop

* fixes for count_cons_of_ne

* fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context)

* bump heartbeats in MathlibTest/observe

* fix, deprecated

* fix merge

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

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* fixes

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

* Trigger CI for leanprover/lean4#7672

* Trigger CI for leanprover/lean4#7672

* update batteries

* Trigger CI for leanprover/lean4#7672

* one fix

* fixes

* maxheartbeats

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* fixes for leanprover/lean4#7672

* cleanups

* .

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

* update aesop

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

* Trigger CI for leanprover/lean4#7690

* Trigger CI for leanprover/lean4#7690

* maxHeartbeats

* max heartbeats

* invalidate cache

* another heartbeats

* bump batteries

* deprecation

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

* Delete

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

* update batteries

* bump batteries

* many more maxHeartbeats

* chore: bump leantar v0.1.15

* invalidate cache

* cache flush, take 2

* feat(Cache): root hash generation counter

* 1-line fix

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

* update deps

* remove upstreamed

* remove all adaptation notes, hooray

* merge lean-pr-testing-7692

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

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

* fix

* Trigger CI for leanprover/lean4#7717

* Trigger CI for leanprover/lean4#7717

* fixes

* fixes

* Trigger CI for leanprover/lean4#7717

* fixes

* fixes

* fixes

* fixes

* got through all of mathlib

* missing space

* fix tests

* Trigger CI for leanprover/lean4#7717

* Trigger CI for leanprover/lean4#7717

* Merge master into nightly-testing

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

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

* Trigger CI for leanprover/lean4#7710

* Trigger CI for leanprover/lean4#7710

* Merge master into nightly-testing

* Trigger CI for leanprover/lean4#7717

* chore: remove fragile tests

* chore: remove fragile tests

* Trigger CI for leanprover/lean4#7710

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

* how did this get dropped?

* Trigger CI for leanprover/lean4#7710

* Trigger CI for leanprover/lean4#7736

* deprecations in Cache

* fix

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

* update batteries

* merge fixes

* fix

* fixes

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

* fix

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

* eliminate some 7717 adaptation notes

* Start fixing, upstream changes needed

* Trigger CI for leanprover/lean4#7756

* Fix

* Fix

* Fix

* Fix

* Trigger CI for leanprover/lean4#7756

* Trigger CI for leanprover/lean4#7756

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

* lake update

* Trigger CI for leanprover/lean4#7756

* Fix

* Fix

* Update batteries

* Fix

* Fix

* Trigger CI for leanprover/lean4#7756

* lake update

* Fix

* Fix

* fix for auxlemma detection

* remove mention of aux proof in Mathlib.Control.Fix

* fix whatsnew

* better fix

* argh

* unfold aux lemmas before transforming aux decls

* fixes

* optimization: abstract nested proofs in toadditive

* docstring

* revert change

* fix merge

* deprecations in shake

* fixes

* fixes

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

* lake update

* fixes

* fix test

* fix

* fix merge

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
@TwoFX TwoFX deleted the markus/nat-gcd branch August 4, 2025 07:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR 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

@TwoFX