English
There is a ring isomorphism between the opposite polynomial ring R[X]ᵐᵒᵖ and the polynomial ring over the opposite ring Rᵐᵒᵖ[X], sending each coefficient to its opposite.
Русский
Существует кольцевой изоморфизм между противоположенным кольцом многочленов R[X]ᵐᵒᵖ и многочленами над противоположным кольцом Rᵐᵒᵖ[X], переводящий каждый коэффициент в его противоположность.
LaTeX
$$$R[X]^{op} \cong (R^{op})[X]$$$
Lean4
/-- Ring isomorphism between `R[X]ᵐᵒᵖ` and `Rᵐᵒᵖ[X]` sending each coefficient of a polynomial
to the corresponding element of the opposite ring. -/
def opRingEquiv (R : Type*) [Semiring R] : R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X] :=
((toFinsuppIso R).op.trans AddMonoidAlgebra.opRingEquiv).trans (toFinsuppIso _).symm
