Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_monomial_mul

∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a * φ) = if n ≤ m then a * (MvPowerSeries.coeff (m - n)) φ else 0

Defined in

Mathlib.RingTheory.MvPowerSeries.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

Semiring