English
The coefficient of degree d in the product of finitely many power series equals a sum over multi-indices of products of coefficients.
Русский
Коэффициент при степени d в произведении конечного числа степенных рядов равен сумме по всем многомерным индексам произведений соответствующих коэффициентов.
LaTeX
$$$\operatorname{coeff}_d\Big(\prod_{j\in s} f_j\Big) = \sum_{l \in \mathrm{finsuppAntidiag}\; s\; d} \prod_{i\in s} \operatorname{coeff}_{l(i)}(f_i)$$$
Lean4
/-- Coefficients of a product of power series -/
theorem coeff_prod [DecidableEq ι] (f : ι → PowerSeries R) (d : ℕ) (s : Finset ι) :
coeff d (∏ j ∈ s, f j) = ∑ l ∈ finsuppAntidiag s d, ∏ i ∈ s, coeff (l i) (f i) :=
by
simp only [coeff]
rw [MvPowerSeries.coeff_prod, ← AddEquiv.finsuppUnique_symm d, ← mapRange_finsuppAntidiag_eq, sum_map, sum_congr rfl]
intro x _
apply prod_congr rfl
intro i _
congr 2
simp only [AddEquiv.toEquiv_eq_coe, Finsupp.mapRange.addEquiv_toEquiv, AddEquiv.toEquiv_symm, Equiv.coe_toEmbedding,
Finsupp.mapRange.equiv_apply, AddEquiv.coe_toEquiv_symm, Finsupp.mapRange_apply, AddEquiv.finsuppUnique_symm]
