English
For algebra equivalences e: A1 ≃ₐ[R] A2 and f: A2 ≃ₐ[R] A3, the induced map on mv-polynomials satisfies mapAlgEquiv σ e followed by mapAlgEquiv σ f equals mapAlgEquiv σ (e.trans f).
Русский
Для алгебраических эквивалентностей e: A1 ≃ₐ[R] A2 и f: A2 ≃ₐ[R] A3 соответствующая отображение на mv-многочленах удовлетворяет: mapAlgEquiv σ e затем mapAlgEquiv σ f равно mapAlgEquiv σ (e.trans f).
LaTeX
$$$$ (mapAlgEquiv \\; \\sigma\\; e).trans (mapAlgEquiv \\; \\sigma\\; f) = mapAlgEquiv \\; \\sigma\\; (e.trans f). $$$$
Lean4
/-- If `e : A ≃+* B` is an isomorphism of rings, then so is `map e`. -/
@[simps apply]
def mapEquiv [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) : MvPolynomial σ S₁ ≃+* MvPolynomial σ S₂ :=
{ map (e : S₁ →+* S₂) with
toFun := map (e : S₁ →+* S₂)
invFun := map (e.symm : S₂ →+* S₁)
left_inv := map_leftInverse e.left_inv
right_inv := map_rightInverse e.right_inv }
