coeff_pow — Mathlib

English

A restatement of the previous coefficient-of-powers formula in an alternative indexing view.

Русский

Переформулировка предыдущей формулы через другую систему индексации.

LaTeX

$$$\\text{(same as above in alternative indexing)}$$$

Lean4

/-- The `d`th coefficient of a power of a multivariate power series
is the sum, indexed by `finsuppAntidiag (Finset.range n) d`, of products of coefficients -/
theorem coeff_pow [DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ} (d : σ →₀ ℕ) :
    coeff d (f ^ n) = ∑ l ∈ finsuppAntidiag (Finset.range n) d, ∏ i ∈ Finset.range n, coeff (l i) f :=
  by
  suffices f ^ n = (Finset.range n).prod fun _ ↦ f by rw [this, coeff_prod]
  rw [Finset.prod_const, card_range]

Похожие утверждения