mathlib3 documentation

ring_theory.polynomial.opposites

Interactions between R[X] and Rᵐᵒᵖ[X] #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the basic API for "pushing through" the isomorphism op_ring_equiv : R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X]. It allows going back and forth between a polynomial ring over a semiring and the polynomial ring over the opposite semiring.

Ring isomorphism between R[X]ᵐᵒᵖ and Rᵐᵒᵖ[X] sending each coefficient of a polynomial to the corresponding element of the opposite ring.

Equations

Lemmas to get started, using op_ring_equiv R on the various expressions of finsupp.single: monomial, C a, X, C a * X ^ n.

Lemmas to get started, using (op_ring_equiv R).symm on the various expressions of finsupp.single: monomial, C a, X, C a * X ^ n.

Lemmas about more global properties of polynomials and opposites.