# Documentation

Mathlib.RingTheory.Polynomial.Opposites

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

This file contains the basic API for "pushing through" the isomorphism opRingEquiv : 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.

def Polynomial.opRingEquiv (R : Type u_2) [] :

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

Instances For

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

@[simp]
theorem Polynomial.opRingEquiv_op_monomial {R : Type u_1} [] (n : ) (r : R) :
↑() (MulOpposite.op (↑() r)) = ↑() ()
@[simp]
theorem Polynomial.opRingEquiv_op_C {R : Type u_1} [] (a : R) :
↑() (MulOpposite.op (Polynomial.C a)) = Polynomial.C ()
@[simp]
theorem Polynomial.opRingEquiv_op_X {R : Type u_1} [] :
↑() (MulOpposite.op Polynomial.X) = Polynomial.X
theorem Polynomial.opRingEquiv_op_C_mul_X_pow {R : Type u_1} [] (r : R) (n : ) :
↑() (MulOpposite.op (Polynomial.C r * Polynomial.X ^ n)) = Polynomial.C () * Polynomial.X ^ n

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

@[simp]
theorem Polynomial.opRingEquiv_symm_monomial {R : Type u_1} [] (n : ) (r : Rᵐᵒᵖ) :
↑() (↑() r) =
@[simp]
theorem Polynomial.opRingEquiv_symm_C {R : Type u_1} [] (a : Rᵐᵒᵖ) :
↑() (Polynomial.C a) = MulOpposite.op (Polynomial.C ())
@[simp]
theorem Polynomial.opRingEquiv_symm_X {R : Type u_1} [] :
↑() Polynomial.X = MulOpposite.op Polynomial.X
theorem Polynomial.opRingEquiv_symm_C_mul_X_pow {R : Type u_1} [] (r : Rᵐᵒᵖ) (n : ) :
↑() (Polynomial.C r * Polynomial.X ^ n) = MulOpposite.op (Polynomial.C () * Polynomial.X ^ n)

Lemmas about more global properties of polynomials and opposites.

@[simp]
theorem Polynomial.coeff_opRingEquiv {R : Type u_1} [] (p : ()ᵐᵒᵖ) (n : ) :
Polynomial.coeff (↑() p) n =
@[simp]
theorem Polynomial.support_opRingEquiv {R : Type u_1} [] (p : ()ᵐᵒᵖ) :
@[simp]
theorem Polynomial.natDegree_opRingEquiv {R : Type u_1} [] (p : ()ᵐᵒᵖ) :
@[simp]
theorem Polynomial.leadingCoeff_opRingEquiv {R : Type u_1} [] (p : ()ᵐᵒᵖ) :