Skip to content

feat: add instance Grind.CommRing (Fin n)#8276

Merged
kim-em merged 15 commits intomasterfrom
grind_fin_commring
May 13, 2025
Merged

feat: add instance Grind.CommRing (Fin n)#8276
kim-em merged 15 commits intomasterfrom
grind_fin_commring

Conversation

@leodemoura
Copy link
Copy Markdown
Member

@leodemoura leodemoura commented May 10, 2025 •
edited
Loading

This PR adds the instances Grind.CommRing (Fin n) and Grind.IsCharP (Fin n) n. New tests:

example (x y z : Fin 13) :
    (x + y + z) ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + 2 * (x * y + y * z + z * x) := by
  grind +ring

example (x y : Fin 17) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x * y * (x + y) := by
  grind +ring

example (x y : Fin 19) : (x - y) * (x ^ 2 + x * y + y ^ 2) = x ^ 3 - y ^ 3 := by
  grind +ring

@leodemoura leodemoura added the changelog-language Language features and metaprograms label May 10, 2025
@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 May 10, 2025
@ghost
Copy link
Copy Markdown

ghost commented May 10, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ddf5512c9a9047d3da4020c6acdf8b28a6b8a892 --onto eabde77d84f9cb065f62e81e057e03792d97f966. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-10 13:32:15)
  • 💥 Mathlib branch lean-pr-testing-8276 build failed against this PR. (2025-05-12 06:08:24) View Log
  • 💥 Mathlib branch lean-pr-testing-8276 build failed against this PR. (2025-05-12 08:00:41) View Log
  • 💥 Mathlib branch lean-pr-testing-8276 build failed against this PR. (2025-05-12 13:13:48) View Log
  • ✅ Mathlib branch lean-pr-testing-8276 has successfully built against this PR. (2025-05-12 22:43:16) View Log
  • 🟡 Mathlib branch lean-pr-testing-8276 build against this PR was cancelled. (2025-05-12 23:40:41) View Log
  • 💥 Mathlib branch lean-pr-testing-8276 build failed against this PR. (2025-05-12 23:49:37) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ef77434a499567372e4bd5a3ab48b98984d56c9d --onto 2b4f372317f214e92988a79fc765586fbfb64e97. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-13 06:02:23)
  • 💥 Mathlib branch lean-pr-testing-8276 build failed against this PR. (2025-05-13 06:17:22) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b04ecaefd7aaa76afd0be59deaf60b98b1346453 --onto 2b4f372317f214e92988a79fc765586fbfb64e97. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-13 11:40:19)
  • 🟡 Mathlib branch lean-pr-testing-8276 build against this PR was cancelled. (2025-05-13 11:51:20) View Log
  • 🟡 Mathlib branch lean-pr-testing-8276 build against this PR was cancelled. (2025-05-13 12:10:15) View Log
  • 💥 Mathlib branch lean-pr-testing-8276 build failed against this PR. (2025-05-13 12:42:12) View Log
  • ❌ Mathlib branch lean-pr-testing-8276 built against this PR, but linting failed. (2025-05-13 21:38:57) View Log

@kim-em kim-em force-pushed the grind_fin_commring branch from 019aa97 to 76c65d9 Compare May 12, 2025 04:53
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 12, 2025
Update lean-toolchain for testing leanprover/lean4#8276
7aa0d8e
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
Update lean-toolchain for testing leanprover/lean4#8276
29eb510
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 12, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 12, 2025
Trigger CI for leanprover/lean4#8276
d22015d
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
Trigger CI for leanprover/lean4#8276
d959104
@kim-em kim-em self-requested a review as a code owner May 12, 2025 12:39
@kim-em kim-em removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 12, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 12, 2025
Trigger CI for leanprover/lean4#8276
13861f8
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
Trigger CI for leanprover/lean4#8276
c1d325b
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 12, 2025
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
@kim-em
fixes for leanprover/lean4#8276
09611ce
@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 May 12, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request May 12, 2025
Trigger CI for leanprover/lean4#8276
3797b35
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
Trigger CI for leanprover/lean4#8276
fc717a8
@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 May 12, 2025
@kim-em kim-em removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels May 13, 2025
@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 May 13, 2025
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request May 13, 2025
@kim-em
fixes for leanprover/lean4#8276
266e103
kim-em added a commit to leanprover-community/batteries that referenced this pull request May 13, 2025
@kim-em
fixes for leanprover/lean4#8276
9f77d71
@kim-em kim-em added this pull request to the merge queue May 13, 2025
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 13, 2025
Merged via the queue into master with commit e0a2667 May 13, 2025
24 checks passed
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

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms 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.

2 participants

@leodemoura @kim-em