Skip to content
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

feat: Nat.lt_pow_self #6200

Merged
merged 2 commits into from
Nov 27, 2024
Merged

feat: Nat.lt_pow_self #6200

merged 2 commits into from
Nov 27, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Nov 24, 2024

This PR upstreams Nat.lt_pow_self and Nat.lt_two_pow from Mathlib and uses them to prove the simp theorem Nat.mod_two_pow.

This simplifies expressions like System.Platform.numBits % 2 ^ System.Platform.numBits = System.Platform.numBits, which is needed for #6188.

@tydeu tydeu added the changelog-library Library label Nov 24, 2024
@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 Nov 24, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 24, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6200
c7de4e5
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 24, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6200
835c294
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 24, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 24, 2024 •
edited
Loading

Mathlib CI status (docs):

@tydeu tydeu added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Nov 24, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 24, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6200
a718748
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 24, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6200
64cdba7
@tydeu tydeu added release-ci Enable all CI checks for a PR, like is done for releases and removed merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. labels Nov 24, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6200
4ab3974
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6200
7dd730c
@tydeu tydeu mentioned this pull request Nov 25, 2024
Draft
tydeu added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2024
@tydeu
chore: adaptions for leanprover/lean4#6200
3f941d8
tydeu added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 25, 2024
@tydeu
chore: adaptions for leanprover/lean4#6200
bb8b98c
@leanprover-community-bot leanprover-community-bot 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 Nov 25, 2024
@tydeu tydeu marked this pull request as ready for review November 25, 2024 02:23
@tydeu tydeu requested a review from kim-em as a code owner November 25, 2024 02:23
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6200
c8eca4f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 26, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6200
5e5178b
@leanprover-community-bot leanprover-community-bot 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 Nov 26, 2024
tydeu added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 26, 2024
@tydeu
chore: review adaptions for leanprover/lean4#6200
c94e3c9
@leanprover-community-bot leanprover-community-bot removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 26, 2024
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 26, 2024
@tydeu tydeu added this pull request to the merge queue Nov 26, 2024
Merged via the queue into leanprover:master with commit 23bec25 Nov 27, 2024
31 checks passed
@tydeu tydeu deleted the nat-lt-pow-self branch November 27, 2024 02:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library release-ci Enable all CI checks for a PR, like is done for releases 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.
3 participants
@tydeu @leanprover-community-bot @kim-em