English
For a finite product S of nonzero terms g(x), the factorization of the product equals the sum of the factorizations: (S.prod g).factorization = S.sum (g x).factorization.
Русский
Для конечного произведения S над функцией g, где каждый g(x) ≠ 0, факторизация произведения равна сумме факторизаций: факторизация(производное) = сумма факторизаций.
LaTeX
$$$ (S.\\mathrm{prod} \\, g).factorization = S.\\mathrm{sum} (\\lambda x. (g x).factorization) \\quad (\\forall x \\in S, g(x) \\neq 0)$$$
Lean4
/-- 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 = 2` and `g = id`. -/
theorem factorization_prod {α : Type*} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
(S.prod g).factorization = S.sum fun x => (g x).factorization := by
classical
ext p
refine Finset.induction_on' S ?_ ?_
· simp
· intro x T hxS hTS hxT IH
have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)
simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]
