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.

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.

    @[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)
    @[simp]
    theorem Polynomial.opRingEquiv_op_X {R : Type u_1} [Semiring R] :
    (Polynomial.opRingEquiv R) (MulOpposite.op Polynomial.X) = Polynomial.X
    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.

    @[simp]
    theorem Polynomial.opRingEquiv_symm_C {R : Type u_1} [Semiring R] (a : Rᵐᵒᵖ) :
    (Polynomial.opRingEquiv R).symm (Polynomial.C a) = MulOpposite.op (Polynomial.C (MulOpposite.unop a))
    @[simp]
    theorem Polynomial.opRingEquiv_symm_X {R : Type u_1} [Semiring R] :
    (Polynomial.opRingEquiv R).symm Polynomial.X = MulOpposite.op Polynomial.X
    theorem Polynomial.opRingEquiv_symm_C_mul_X_pow {R : Type u_1} [Semiring R] (r : Rᵐᵒᵖ) (n : ) :
    (Polynomial.opRingEquiv R).symm (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.

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