Skip to content

feat: add LawfulOfScientific class #10971

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
kim-em merged 1 commit into from
Oct 27, 2025
Merged

feat: add LawfulOfScientific class #10971

kim-em merged 1 commit into from
Oct 27, 2025

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Oct 26, 2025

This PR adds a LawfulOfScientific class, providing compatibility with a Lean.Grind.Field structure.

@kim-em kim-em added the changelog-tactics User facing tactics label Oct 26, 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 Oct 26, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 26, 2025 •
edited
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 4887eeb77c7b67507faa31a0bc65e7f76473a7aa --onto 97d63db52cd2fc3353f8a75f48209de0011f1bd3. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-26 12:15:04)
  • ✅ Mathlib branch lean-pr-testing-10971 has successfully built against this PR. (2025-10-27 00:32:15) View Log
  • 🟡 Mathlib branch lean-pr-testing-10971 build this PR didn't complete normally. (2025-10-27 04:16:41) View Log
  • 🟡 Mathlib branch lean-pr-testing-10971 build this PR didn't complete normally. (2025-10-27 04:18:35) View Log
  • ✅ Mathlib branch lean-pr-testing-10971 has successfully built against this PR. (2025-10-27 04:59:44) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 26, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4887eeb77c7b67507faa31a0bc65e7f76473a7aa --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-26 12:15:06)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-26 23:25:59)

@kim-em kim-em added this pull request to the merge queue Oct 26, 2025
@kim-em kim-em removed this pull request from the merge queue due to a manual request Oct 26, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10971
56e8dbf
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10971
836f923
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 27, 2025
@kim-em kim-em mentioned this pull request Oct 27, 2025
Closed
@kim-em kim-em added this pull request to the merge queue Oct 27, 2025
Merged via the queue into master with commit 30ecacd Oct 27, 2025
22 checks passed
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
@kim-em @wkrozowski
feat: add LawfulOfScientific class (leanprover#10971)
87e18fb 
This PR adds a `LawfulOfScientific` class, providing compatibility with
a `Lean.Grind.Field` structure.
@nomeata nomeata mentioned this pull request Oct 29, 2025
Merged
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Oct 31, 2025
@kim-em
feat: preparations for LawfulOfScientific (#30958)
e280942 
`LawfulOfScientific`, and grind support for it, will be added shortly. This is PR contains the prerequisites which can already go in `master`.

c.f. leanprover/lean4#10971 and the [`lean-pr-testing-10971`](leanprover-community@4f3ca51) branch.
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@kim-em @BeibeiX0
feat: preparations for LawfulOfScientific (leanprover-community#30958)
2c3e254 
`LawfulOfScientific`, and grind support for it, will be added shortly. This is PR contains the prerequisites which can already go in `master`.

c.f. leanprover/lean4#10971 and the [`lean-pr-testing-10971`](leanprover-community@4f3ca51) branch.
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

builds-mathlib CI has verified that Mathlib builds against this PR changelog-tactics User facing tactics 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.

4 participants

@kim-em @leanprover-community-bot @leanprover-bot