Theorems · Theorem · commutative algebra

PowerSeries.subst_rescale_of_degree_eq_one

∀ {R : Type u_2} [inst : CommRing R] (a : R) {σ : Type u_7} (p : MvPowerSeries σ R),
  (∀ d ∈ Function.support p, Finsupp.degree d = 1) →
    ∀ (f : PowerSeries R),
      PowerSeries.subst p ((PowerSeries.rescale a) f) =
        (MvPowerSeries.rescale (Function.const σ a)) (PowerSeries.subst p f)

Substitution by p commutes with scalar homothety.

Defined in

Mathlib.RingTheory.PowerSeries.Substitution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing