Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_rescale

∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (f : MvPowerSeries σ R) (a : σ → R) (n : σ →₀ ℕ),
  (MvPowerSeries.coeff n) ((MvPowerSeries.rescale a) f) = (n.prod fun s m => a s ^ m) * (MvPowerSeries.coeff n) f

Defined in

Mathlib.RingTheory.MvPowerSeries.Substitution

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiring