Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_expand_smul

∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R) (m : σ →₀ ℕ),
  (MvPowerSeries.coeff (p • m)) ((MvPowerSeries.expand p hp) φ) = (MvPowerSeries.coeff m) φ

Defined in

Mathlib.RingTheory.MvPowerSeries.Expand

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRing