English
Let R be a commutative semiring and A,B be R-algebras. If A and B are isomorphic as R-algebras, then their polynomial rings are also isomorphic as R-algebras; the isomorphism is obtained by applying the algebra isomorphism to each coefficient.
Русский
Пусть R — коммутативное полупрямое кольцо, A и B — R-алгебры. Если A и B изоморфны как R-алгебры, то их кольца многочленов над R также изоморфны как R-алгебры; изоморфизм получается при отображении коэффициентов через существующий изоморфизм.
LaTeX
$$$$\forall f:\ A \simeq_R B,\; \Polynomial A \simeq_R \Polynomial B.$$$$
Lean4
/-- If `A` and `B` are isomorphic as `R`-algebras, then so are their polynomial rings -/
def mapAlgEquiv (f : A ≃ₐ[R] B) : Polynomial A ≃ₐ[R] Polynomial B :=
AlgEquiv.ofAlgHom (mapAlgHom f.toAlgHom) (mapAlgHom f.symm.toAlgHom) (by simp) (by simp)
