feat: `Int.gcd`/`Int.lcm` lemmas by TwoFX · Pull Request #7802 · leanprover/lean4

TwoFX · 2025-04-03T14:37:08Z

This PR adds Int.gcd and Int.lcm variants of all Nat.gcd and Nat.lcm lemmas.

ghost · 2025-04-03T15:26:58Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 83067d67d65efe4818205ddb3f9b2ab824735b10 --onto 1ee7e1a9d8a67d1d8dcf6a17ac5c92bc2c7e0fac. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-03 15:26:57)
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 06:23:09) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 06:57:17) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 08:21:44) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 09:02:19) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 10:36:13) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 10:43:03) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 11:09:13) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 11:30:10) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 11:38:05) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 11:56:51) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 12:06:57) View Log
💥 Mathlib branch lean-pr-testing-7802 build failed against this PR. (2025-04-04 12:23:27) View Log
✅ Mathlib branch lean-pr-testing-7802 has successfully built against this PR. (2025-04-04 12:31:41) View Log

* fixes * fix test * fix * chore: adaptations for leanprover/lean4#7797 * stricter rfl check * fix merge * Trigger CI for leanprover/lean4#7797 * Trigger CI for leanprover/lean4#7797 * Trigger CI for leanprover/lean4#7797 * inverse construction * Update lean-toolchain for testing leanprover/lean4#7791 * lake update * Fix * Fix * Fix * chore: bump to nightly-2025-04-03 * more fixes * merge lean-pr-testing-6325 * bump proofwidgets * Update lean-toolchain for testing leanprover/lean4#7812 * shake * fix shake * fix tests * import mathlib.init * Update lean-toolchain for testing leanprover/lean4#7816 * Trigger CI for leanprover/lean4#7816 * Update lean-toolchain for testing leanprover/lean4#7802 * Fix * fixes * Fix (pending upstream changes) * Trigger CI for leanprover/lean4#7802 * fix * chore: bump to nightly-2025-04-04 * Fix * Fix * Fix * Fix * Fix * Fix * Update lean-toolchain for testing leanprover/lean4#7818 * Fix * Fix * Fix * Merge master into nightly-testing * Fix * Fix comments * fixes * Trigger CI for leanprover/lean4#7816 * fix * fix * missing doc-string? * chore: bump to nightly-2025-04-05 * chore: bump to nightly-2025-04-06 * move Batteries to nightly-testing * lake update * lint * fix * chore: bump to nightly-2025-04-07 * sprinkle noncomputable * fix: relativize file paths fix for leanprover/lean4#7822 * chore: reset cache * chore: bump to nightly-2025-04-07 * shake * fix: relativize more * Update lean-toolchain for testing leanprover/lean4#7856 * Update lean-toolchain for testing leanprover/lean4#7851 * Fix * Fix * Fix * Fix * chore: bump to nightly-2025-04-08 * Update lean-toolchain for testing leanprover/lean4#7870 * Trigger CI for leanprover/lean4#7870 * Trigger CI for leanprover/lean4#7870 * Trigger CI for leanprover/lean4#7870 * wip * Trigger CI for leanprover/lean4#7870 * . * chore: bump to nightly-2025-04-09 * Trigger CI for leanprover/lean4#7870 * . * bump * lake update * fixes for leanprover/lean4#7873 * fixes * deprecations * chore: bump to nightly-2025-04-10 * chore: `Option.zipWith` -> `Option.merge` * lake update * toolchain * fix * fix * Update lean-toolchain for testing leanprover/lean4#7897 * Trigger CI for leanprover/lean4#7897 * fix * lake update and fix * Fix * Fix * Trigger CI for leanprover/lean4#7897 * fix merge * chore: adaptations for nightly-2025-04-10 * chore: bump to nightly-2025-04-14 * fix * . * annotate changed goal state * fixes (adaptation notes) * cleanup imports * cleanup * Update lean-toolchain for testing leanprover/lean4#7933 * Fix * Fix * Update lean-toolchain for testing leanprover/lean4#7975 * remove adaptation notes * chore: bump to nightly-2025-04-16 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com>

TwoFX force-pushed the markus/int-gcd branch from 3b9f714 to 8619a88 Compare April 3, 2025 14:39

github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 3, 2025 15:19 Inactive

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 3, 2025

gcd lemmas

2fab493

TwoFX force-pushed the markus/int-gcd branch from e495108 to 2fab493 Compare April 4, 2025 05:43

github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 4, 2025 05:55 Inactive

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 4, 2025

Update lean-toolchain for testing leanprover/lean4#7802

bf4498d

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 4, 2025

Update lean-toolchain for testing leanprover/lean4#7802

fbdcb56

ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 4, 2025

Changes after mathlib adaptations

9ba5f03

github-actions bot temporarily deployed to lean-lang.org/lean4/doc April 4, 2025 08:32 Inactive

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Apr 4, 2025

Trigger CI for leanprover/lean4#7802

fb3327d

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 4, 2025

Trigger CI for leanprover/lean4#7802

fcdb09f

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 4, 2025

TwoFX marked this pull request as ready for review April 4, 2025 12:39

TwoFX requested a review from kim-em as a code owner April 4, 2025 12:39

TwoFX enabled auto-merge April 4, 2025 12:39

TwoFX added the changelog-library Library label Apr 4, 2025

TwoFX added this pull request to the merge queue Apr 4, 2025

Merged via the queue into master with commit 674c7ef Apr 4, 2025
27 of 28 checks passed

TwoFX mentioned this pull request Apr 8, 2025

Nat.gcd_le_left and Nat.gcd_le_right have inconsistent implicit parameters #7867

Closed

3 tasks

TwoFX deleted the markus/int-gcd branch August 4, 2025 07:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: `Int.gcd`/`Int.lcm` lemmas#7802

feat: `Int.gcd`/`Int.lcm` lemmas#7802
TwoFX merged 2 commits intomasterfrom
markus/int-gcd

TwoFX commented Apr 3, 2025

Uh oh!

ghost commented Apr 3, 2025 •

edited by ghost

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

TwoFX commented Apr 3, 2025

Uh oh!

ghost commented Apr 3, 2025 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

ghost commented Apr 3, 2025 •

edited by ghost

Loading