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] - feat(data/nat/factorization/basic): define ord_proj[p]
and ord_compl[p]
, prove basic lemmas
#15589
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.
Could you add a description of the changed declarations to the PR description, in particular explaining the renames?
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.
Thanks!
bors r+
…pl[p]`, prove basic lemmas (#15589) `ord_proj[p] n := p ^ (nat.factorization n p)` is the largest power of `p` that divides into `n`. For `p = 2` this is the even part of `n`. `ord_compl[p] n := n / ord_proj[p] n` is the largest divisor of `n` not divisible by `p`. For `p = 2` this is the odd part of `n`. Note that for consistency with the naming of other lemmas introduced in this PR, the following lemmas are renamed: * `pow_factorization_dvd` -> `ord_proj_dvd` * `pow_factorization_le` -> `ord_proj_le` * `not_dvd_div_pow_factorization` -> `not_dvd_ord_compl` * `coprime_of_div_pow_factorization` -> `coprime_ord_compl` * `div_pow_factorization_ne_zero` -> `ord_compl_pos` * `prime.pow_dvd_iff_dvd_pow_factorization` -> `prime.pow_dvd_iff_dvd_ord_proj`
Pull request successfully merged into master. Build succeeded: |
ord_proj[p]
and ord_compl[p]
, prove basic lemmasord_proj[p]
and ord_compl[p]
, prove basic lemmas
Resolving merge conflict after #15589
ord_proj[p] n := p ^ (nat.factorization n p)
is the largest power ofp
that divides inton
. Forp = 2
this is the even part ofn
.ord_compl[p] n := n / ord_proj[p] n
is the largest divisor ofn
not divisible byp
. Forp = 2
this is the odd part ofn
.Note that for consistency with the naming of other lemmas introduced in this PR, the following lemmas are renamed:
pow_factorization_dvd
->ord_proj_dvd
pow_factorization_le
->ord_proj_le
not_dvd_div_pow_factorization
->not_dvd_ord_compl
coprime_of_div_pow_factorization
->coprime_ord_compl
div_pow_factorization_ne_zero
->ord_compl_pos
prime.pow_dvd_iff_dvd_pow_factorization
->prime.pow_dvd_iff_dvd_ord_proj