Commit 2022-08-17 09:39 6c135283

feat(data/nat/factorization/basic): define ord_proj[p] and ord_compl[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