-
Notifications
You must be signed in to change notification settings - Fork 298
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.
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
[Merged by Bors] - refactor(number_theory/primorial): split the proof, golf it #18238
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For future reference, can you add to the PR description a proof of dvd_choose_of_middling_prime
from your new lemmas?
Done. Also forward-ported. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you, that's perfect!
More lemmas, less lines. The kind of PRs I like to see.
maintainer merge
Oh wait, sorry. It seemed that merge conflicts just happened. |
I'll look into this tonight. |
bors d+ |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
* Add `nat.prime.dvd_choose`, delete less general `dvd_choose_of_middling_prime`. * Add `primorial_pos`, `primorial_add`, `primorial_add_dvd`, and `primorial_add_le`. * Golf some proofs. Here is a proof of `dvd_choose_of_middling_prime` based on `nat.prime.dvd_choose`: ```lean open nat lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ) (p_big : m + 1 < p) (p_small : p ≤ 2 * m + 1) : p ∣ choose (2 * m + 1) (m + 1) := is_prime.dvd_choose p_big (by simpa [two_mul] using p_big.le) p_small ``` Forward-ported in leanprover-community/mathlib4#1770
Pull request successfully merged into master. Build succeeded: |
This is a forward-port of leanprover-community/mathlib#18238
nat.prime.dvd_choose
, delete less generaldvd_choose_of_middling_prime
.primorial_pos
,primorial_add
,primorial_add_dvd
, andprimorial_add_le
.Here is a proof of
dvd_choose_of_middling_prime
based onnat.prime.dvd_choose
:Forward-ported in leanprover-community/mathlib4#1770