Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_pow

∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ}
  (d : σ →₀ ℕ),
  (MvPowerSeries.coeff d) (f ^ n) =
    ∑ l ∈ (Finset.range n).finsuppAntidiag d, ∏ i ∈ Finset.range n, (MvPowerSeries.coeff (l i)) f

The dth coefficient of a power of a multivariate power series is the sum, indexed by finsuppAntidiag (Finset.range n) d, of products of coefficients

Defined in

Mathlib.RingTheory.MvPowerSeries.Basic

Cited by

1 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringDecidableEq