mathlib3

6c135283 - feat(data/nat/factorization/basic): define `ord_proj[p]` and `ord_compl[p]`, prove basic lemmas (#15589)

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`