Skip to content

feat: add msb_neg_of_msb_false, msb_neg_of_msb_true, msb_neg_umod_neg_of_msb_true_of_msb_true, msg_neg_neg_mod_neg #8376

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
Draft
wants to merge 77 commits into
base: master
Choose a base branch
from
Draft

feat: add msb_neg_of_msb_false, msb_neg_of_msb_true, msb_neg_umod_neg_of_msb_true_of_msb_true, msg_neg_neg_mod_neg #8376

wants to merge 77 commits into from

Conversation

luisacicolini
Copy link
Contributor

No description provided.

luisacicolini and others added 30 commits May 7, 2025 08:20
@luisacicolini
feat: statement
2cb11fe
@luisacicolini
chore:wip
8ab06cf
@luisacicolini
chore: first case
2da1672
@luisacicolini
chore: progress
f69d8cc
@luisacicolini
chore: first case solved
6d30b11
@luisacicolini
chore: couple smaller cases
193c0de
@luisacicolini
chore: wip
e13c792
@luisacicolini
chore: useless theorem
5469f7d
@tobiasgrosser
reduce the proof a bit
df4a406
@luisacicolini
chore: case three converts to emod
d3d84a0
@luisacicolini
chore: case three subcase one
96206b6
@luisacicolini
chore: progress
1a637c4
@luisacicolini
chore: wip
54d2a2d
@luisacicolini
chore: wip
6e460eb
@luisacicolini
chore: wip
c057e06
@tobiasgrosser
chore: add proof structure
6f809ed
@tobiasgrosser
Clarify where to apply the bmod
1572cae
@luisacicolini
chore: first split case
2f5b90b
@tobiasgrosser
template for last case
4ef5a02
@luisacicolini
chore: push
6081d20
@luisacicolini
chore: case 1/4
b46492e
@luisacicolini
chore: case 2/4
1d8da7f
@luisacicolini
chore: case 3/4
86bf9f2
@tobiasgrosser
build up umod_msb theory
aa22067
@luisacicolini
chore: completed case 3
f3d0b00
@tobiasgrosser
more cleanup
d5b6eac
@luisacicolini
chore: case 2, pt 1
35a0576
@tobiasgrosser
another msb_neg statement
ac4b4b4
@luisacicolini
chore: case 2
707748a
@luisacicolini
chore: case 2
2b39e65
luisacicolini and others added 27 commits May 14, 2025 20:58
@luisacicolini
chore: cleanup 2/?, all those norm_casts...
ac8154f
@luisacicolini
chore: cleanup 1 and 2
a3bae6f
@luisacicolini
chore: cleanup 3/?
35ec0b5
@luisacicolini
chore: more cleanup 4/?
a487d51
@luisacicolini
chore: cleanup first case 5/?
818503c
@luisacicolini
chore: more cleanup, 5/?
92749e1
@luisacicolini
chore: cleanup 6/?
72ac9c0
@luisacicolini
chore: cleanup 7/? main theorem
5aca481
@luisacicolini
chore: cleanup 8/?
3f9727d
@luisacicolini
chore: simp only
fa23385
@luisacicolini
Merge branch 'leanprover:master' into toInt-smod
37f24bb
@luisacicolini
chore: remove unused theorem
858aae9
@tobiasgrosser
shorten the proof
2e896b3
@tobiasgrosser
shorten the proof
d9f5d78
@tobiasgrosser
drop unused statements
b22b9a7
@tobiasgrosser
clean further
e46ac9b
@tobiasgrosser
Format toInt_smod better
456bb3a
@tobiasgrosser
Shorten further
98b14c6
@tobiasgrosser
Shorten further
fd95519
@tobiasgrosser
related mod and dvd
8179228
@tobiasgrosser
shorten further
2bb786a
@tobiasgrosser
drop an unnecessary case
13caeee
@tobiasgrosser
clean
7540e67
@tobiasgrosser
clean
a66acc1
@luisacicolini
chore: comments and naming
e131348
@luisacicolini
chore: unused theorems
65ad40f
@luisacicolini
chore: move theorems from previous pr
d8c1b85
@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 16, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto 6ca31baa55e4b29c9667085736863f9ca840b16c. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-16 09:01:05)

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 will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees
No one assigned
Labels
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
@luisacicolini @leanprover-community-bot @tobiasgrosser