English
The d-th coefficient of f^n equals the sum over finsuppAntidiag of Finset.range n of products of coefficients: coeff d (f^n) = ∑ l ∈ finsuppAntidiag (Finset.range n) d, ∏_{i ∈ Finset.range n} coeff (l i) f.
Русский
d-й коэффициент f^n выражается как сумма по finsuppAntidiag(range n) через произведения коэффициентов f.
LaTeX
$$$\\operatorname{coeff} d\\,(f^n) = \\sum_{l \\in \\mathrm{finsuppAntidiag}(\\mathrm{Range}(n))} \\prod_{i\\in \\mathrm{Range}(n)} \\operatorname{coeff}(l_i) f$$$
Lean4
theorem prod_monomial (f : ι → σ →₀ ℕ) (g : ι → R) (s : Finset ι) :
∏ i ∈ s, monomial (f i) (g i) = monomial (∑ i ∈ s, f i) (∏ i ∈ s, g i) := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha h => simp [h, monomial_mul_monomial]
