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.

source
def Polynomial.opRingEquiv (R : Type u_2) [Semiring R] :
(Polynomial R)ᵐᵒᵖ ≃+* Polynomial 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 opRingEquiv R on the various expressions of Finsupp.single: monomial, C a, X, C a * X ^ n.

source
@[simp]
theorem Polynomial.opRingEquiv_op_monomial {R : Type u_1} [Semiring R] (n : ℕ) (r : R) :
(opRingEquiv R) (MulOpposite.op ((monomial n) r)) = (monomial n) (MulOpposite.op r)
source
@[simp]
theorem Polynomial.opRingEquiv_op_C {R : Type u_1} [Semiring R] (a : R) :
(opRingEquiv R) (MulOpposite.op (C a)) = C (MulOpposite.op a)
source
@[simp]
theorem Polynomial.opRingEquiv_op_X {R : Type u_1} [Semiring R] :
(opRingEquiv R) (MulOpposite.op X) = X
source
theorem Polynomial.opRingEquiv_op_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) :
(opRingEquiv R) (MulOpposite.op (C r * X ^ n)) = C (MulOpposite.op r) * 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.

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

Lemmas about more global properties of polynomials and opposites.

source
@[simp]
theorem Polynomial.coeff_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) (n : ℕ) :
((opRingEquiv R) p).coeff n = MulOpposite.op ((MulOpposite.unop p).coeff n)
source
@[simp]
theorem Polynomial.support_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) :
((opRingEquiv R) p).support = (MulOpposite.unop p).support
source
@[simp]
theorem Polynomial.natDegree_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) :
((opRingEquiv R) p).natDegree = (MulOpposite.unop p).natDegree
source
@[simp]
theorem Polynomial.leadingCoeff_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) :
((opRingEquiv R) p).leadingCoeff = MulOpposite.op (MulOpposite.unop p).leadingCoeff