Commit 2022-05-12 20:54 86d58ae7

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 in Zulip