Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_C_mul

∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
  (MvPowerSeries.coeff n) (MvPowerSeries.C a * φ) = a * (MvPowerSeries.coeff n) φ

Defined in

Mathlib.RingTheory.MvPowerSeries.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

Semiring