English
For algebra equivalences e: A1 ≃ₐ[R] A2 and f: A2 ≃ₐ[R] A3, the induced map on mv-polynomials satisfies mapEquiv σ e composed with mapEquiv σ f equals mapEquiv σ (e.trans f).
Русский
Для эквивалентностей A1 ≃ₐ[A] A2 и A2 ≃ₐ[R] A3 соответствующее отображение mv-многочленов удовлетворяет: mapEquiv σ e ∘ mapEquiv σ f = mapEquiv σ (e.trans f).
LaTeX
$$$$ (mapEquiv \\; σ\\; e) \\circ (mapEquiv \\; σ\\; f) = mapEquiv \\; σ\\; (e \\circ f). $$$$
Lean4
@[simp]
theorem mapEquiv_trans [CommSemiring S₁] [CommSemiring S₂] [CommSemiring S₃] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :
(mapEquiv σ e).trans (mapEquiv σ f) = mapEquiv σ (e.trans f) :=
RingEquiv.ext fun p => by
simp only [RingEquiv.coe_trans, comp_apply, mapEquiv_apply, RingEquiv.coe_ringHom_trans, map_map]
