mathlib3

261c24c6 - feat(data/nat/factorization/basic): add lemma `factorization_eq_card_pow_dvd` (#15014)

feat(data/nat/factorization/basic): add lemma `factorization_eq_card_pow_dvd` (#15014) Adds lemma `factorization_eq_card_pow_dvd (pp : p.prime) : n.factorization p = ((Ico 1 n).filter (λ i, p ^ i ∣ n)).card` This is a counterpart to `multiplicity_eq_card_pow_dvd` defined and proved in terms of `factorization`. Also proves some upper bounds on `n.factorization p`: `factorization_lt (hn : n ≠ 0) : n.factorization p < n` `factorization_le_of_le_pow (hb : n ≤ p ^ b) : n.factorization p ≤ b` Co-authored-by: Kyle Miller <kmill31415@gmail.com>