English
The coefficient of a product over a finite index set s is the sum over all compatible index assignments of products of coefficients: coeff d (∏_{i∈s} f_i) = ∑_{l∈finsuppAntidiag s d} ∏_{i∈s} coeff (l_i) (f_i).
Русский
Коэффициент произведения равен сумме по всем совместимым присваиваниям индексов произведений коэффициентов: ...
LaTeX
$$$\\operatorname{coeff} d\\big( \\prod_{i\\in s} f_i \\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 ι] [DecidableEq σ] (f : ι → MvPowerSeries σ R) (d : σ →₀ ℕ) (s : Finset ι) :
coeff d (∏ j ∈ s, f j) = ∑ l ∈ finsuppAntidiag s d, ∏ i ∈ s, coeff (l i) (f i) := by
induction s using Finset.induction_on generalizing d with
| empty =>
simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]
split_ifs
· simp only [card_singleton, Nat.cast_one]
· simp only [card_empty, Nat.cast_zero]
| insert a s ha ih =>
rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
· apply Finset.sum_congr rfl
simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
rintro u v rfl
rw [ih, Finset.mul_sum, ← Finset.sum_attach]
apply Finset.sum_congr rfl
simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left, Subtype.forall]
rintro x -
rw [Finset.prod_congr rfl]
intro i hi
rw [Function.update_of_ne]
exact ne_of_mem_of_not_mem hi ha
· simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq, disjoint_left, mem_map,
mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists, exists_prop, not_exists, not_and,
forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Prod.forall, Prod.mk.injEq]
rintro u v rfl u' v' huv h k - l - hkl
obtain rfl : u' = u := by simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
simp only [add_right_inj] at huv
exact h rfl huv.symm
