English
Let R and N be commutative semirings with an R-algebra structure on N, and let σ be a set. Then the R-algebra MvPolynomial(σ, R) tensored with N over R is algebraically isomorphic to the polynomial algebra MvPolynomial(σ, N).
Русский
Пусть R и N — коммутативные полусх, имеется структура R-алгебры на N, и возьмём σ. Тогда тензорное произведение алгебры многочленов MvPolynomial(σ, R) над R с N изоморфно алгебраически алгебре MvPolynomial(σ, N).
LaTeX
$$$ (MvPolynomial\\ kernel{\\sigma}{R}) \\otimes_R N \\cong_R MvPolynomial(\\sigma, N) $$$
Lean4
/-- The tensor product of the polynomial algebra by an algebra
is algebraically equivalent to a polynomial algebra with
coefficients in that algebra -/
noncomputable def scalarRTensorAlgEquiv : MvPolynomial σ R ⊗[R] N ≃ₐ[R] MvPolynomial σ N :=
rTensorAlgEquiv.trans (mapAlgEquiv σ (Algebra.TensorProduct.lid R N))
