Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_mul_monomial

∀ {σ : 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 (MvPowerSeries.coeff (m - n)) φ * a else 0

Defined in

Mathlib.RingTheory.MvPowerSeries.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

Semiring