mathlib3

975031d5 - feat(data/nat/factorization): add lemma `factorization_prod` (#11395)

feat(data/nat/factorization): add lemma `factorization_prod` (#11395) For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : finset α`, the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`. Generalises `factorization_mul`, which is the special case where `S.card = 2` and `g = id`.