Theorems · Theorem · commutative algebra

PowerSeries.coeff_pow

∀ {R : Type u_2} [inst : CommSemiring R] (k n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff n) (φ ^ k) =
    ∑ l ∈ (Finset.range k).finsuppAntidiag n, ∏ i ∈ Finset.range k, (PowerSeries.coeff (l i)) φ

The n-th coefficient of the k-th power of a power series.

Defined in

Mathlib.RingTheory.PowerSeries.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiring