Theorems · Theorem · commutative algebra

PowerSeries.rescale_map

∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (φ : R →+* S) (r : R)
  (f : PowerSeries R),
  (PowerSeries.rescale (φ r)) ((PowerSeries.map φ) f) = (PowerSeries.map φ) ((PowerSeries.rescale r) f)

Defined in

Mathlib.RingTheory.PowerSeries.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring