# mathlib3documentation

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.

noncomputable def polynomial.op_ring_equiv (R : Type u_1) [semiring R] :

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.

@[simp]
theorem polynomial.op_ring_equiv_op_monomial {R : Type u_1} [semiring R] (n : ) (r : R) :
@[simp]
theorem polynomial.op_ring_equiv_op_C {R : Type u_1} [semiring R] (a : R) :
@[simp]
theorem polynomial.op_ring_equiv_op_X {R : Type u_1} [semiring R] :
theorem polynomial.op_ring_equiv_op_C_mul_X_pow {R : Type u_1} [semiring R] (r : R) (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.

@[simp]
theorem polynomial.op_ring_equiv_symm_monomial {R : Type u_1} [semiring R] (n : ) (r : Rᵐᵒᵖ) :
( r) =
@[simp]
theorem polynomial.op_ring_equiv_symm_C {R : Type u_1} [semiring R] (a : Rᵐᵒᵖ) :
@[simp]
theorem polynomial.op_ring_equiv_symm_X {R : Type u_1} [semiring R] :

Lemmas about more global properties of polynomials and opposites.

@[simp]
theorem polynomial.coeff_op_ring_equiv {R : Type u_1} [semiring R] (p : (polynomial R)ᵐᵒᵖ) (n : ) :
p).coeff n =
@[simp]
@[simp]