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
Instances For

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

    source
    @[simp]
    theorem Polynomial.opRingEquiv_symm_monomial {R : Type u_1} [Semiring R] (n : ℕ) (r : Rᵐᵒᵖ) :
    (RingEquiv.symm (Polynomial.opRingEquiv R)) ((Polynomial.monomial n) r) = MulOpposite.op ((Polynomial.monomial n) (MulOpposite.unop r))
    source
    @[simp]
    theorem Polynomial.opRingEquiv_symm_C {R : Type u_1} [Semiring R] (a : Rᵐᵒᵖ) :
    (RingEquiv.symm (Polynomial.opRingEquiv R)) (Polynomial.C a) = MulOpposite.op (Polynomial.C (MulOpposite.unop a))
    source
    @[simp]
    theorem Polynomial.opRingEquiv_symm_X {R : Type u_1} [Semiring R] :
    (RingEquiv.symm (Polynomial.opRingEquiv R)) Polynomial.X = MulOpposite.op Polynomial.X
    source
    theorem Polynomial.opRingEquiv_symm_C_mul_X_pow {R : Type u_1} [Semiring R] (r : Rᵐᵒᵖ) (n : ℕ) :
    (RingEquiv.symm (Polynomial.opRingEquiv R)) (Polynomial.C r * Polynomial.X ^ n) = MulOpposite.op (Polynomial.C (MulOpposite.unop r) * Polynomial.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 : ℕ) :
    Polynomial.coeff ((Polynomial.opRingEquiv R) p) n = MulOpposite.op (Polynomial.coeff (MulOpposite.unop p) n)
    source
    @[simp]
    theorem Polynomial.support_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) :
    Polynomial.support ((Polynomial.opRingEquiv R) p) = Polynomial.support (MulOpposite.unop p)
    source
    @[simp]
    theorem Polynomial.natDegree_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) :
    Polynomial.natDegree ((Polynomial.opRingEquiv R) p) = Polynomial.natDegree (MulOpposite.unop p)
    source
    @[simp]
    theorem Polynomial.leadingCoeff_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) :
    Polynomial.leadingCoeff ((Polynomial.opRingEquiv R) p) = MulOpposite.op (Polynomial.leadingCoeff (MulOpposite.unop p))