Theorems · Theorem · commutative algebra

MvPowerSeries.renameEquiv_apply

∀ {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (e : σ ≃ τ) (a : MvPowerSeries σ R),
  (MvPowerSeries.renameEquiv R e) a = (↑↑(MvPowerSeries.rename ⇑e).toRingHom).toFun a

Defined in

Mathlib.RingTheory.MvPowerSeries.Rename

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiring