Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`.
- Loading branch information