Theorems · Theorem · commutative algebra

MvPowerSeries.expand_comp_substAlgHom

∀ {σ : Type u_1} {τ : Type u_2} {S : Type u_4} [inst : CommRing S] (p : ℕ) (hp : p ≠ 0) {f : σ → MvPowerSeries τ S}
  (hf : MvPowerSeries.HasSubst f),
  (MvPowerSeries.expand p hp).comp (MvPowerSeries.substAlgHom hf) = MvPowerSeries.substAlgHom ⋯

Defined in

Mathlib.RingTheory.MvPowerSeries.Expand

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing