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.
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}
[Semiring R]
(n : ℕ)
(r : R)
:
↑(Polynomial.opRingEquiv R) (MulOpposite.op (↑(Polynomial.monomial n) r)) = ↑(Polynomial.monomial n) (MulOpposite.op r)
@[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_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))
@[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))
@[simp]
theorem
Polynomial.opRingEquiv_symm_X
{R : Type u_1}
[Semiring R]
:
↑(RingEquiv.symm (Polynomial.opRingEquiv R)) Polynomial.X = MulOpposite.op Polynomial.X
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.
@[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)
@[simp]
@[simp]
@[simp]