mathlib

86d58ae7 - feat(data/nat/factorization): three lemmas on the components of factorizations (#14031)

feat(data/nat/factorization): three lemmas on the components of factorizations (#14031) `pow_factorization_le : p ^ (n.factorization) p ≤ n` `div_pow_factorization_ne_zero : n / p ^ (n.factorization) p ≠ 0` `not_dvd_div_pow_factorization : ¬p ∣ n / p ^ (n.factorization) p` Prompted by [this question](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/prime.20factorisation) in Zulip