Interactions between R[X] and Rᵐᵒᵖ[X] #
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] :
(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.
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) :
⇑(polynomial.op_ring_equiv R) (mul_opposite.op (⇑(polynomial.monomial n) r)) = ⇑(polynomial.monomial n) (mul_opposite.op r)
@[simp]
@[simp]
theorem
polynomial.op_ring_equiv_op_C_mul_X_pow
{R : Type u_1}
[semiring R]
(r : R)
(n : ℕ) :
⇑(polynomial.op_ring_equiv R) (mul_opposite.op (⇑polynomial.C r * polynomial.X ^ n)) = ⇑polynomial.C (mul_opposite.op r) * polynomial.X ^ 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ᵐᵒᵖ) :
⇑((polynomial.op_ring_equiv R).symm) (⇑(polynomial.monomial n) r) = mul_opposite.op (⇑(polynomial.monomial n) (mul_opposite.unop r))
@[simp]
theorem
polynomial.op_ring_equiv_symm_C
{R : Type u_1}
[semiring R]
(a : Rᵐᵒᵖ) :
⇑((polynomial.op_ring_equiv R).symm) (⇑polynomial.C a) = mul_opposite.op (⇑polynomial.C (mul_opposite.unop a))
@[simp]
theorem
polynomial.op_ring_equiv_symm_C_mul_X_pow
{R : Type u_1}
[semiring R]
(r : Rᵐᵒᵖ)
(n : ℕ) :
⇑((polynomial.op_ring_equiv R).symm) (⇑polynomial.C r * polynomial.X ^ n) = mul_opposite.op (⇑polynomial.C (mul_opposite.unop r) * polynomial.X ^ n)
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 : ℕ) :
(⇑(polynomial.op_ring_equiv R) p).coeff n = mul_opposite.op ((mul_opposite.unop p).coeff n)
@[simp]
theorem
polynomial.support_op_ring_equiv
{R : Type u_1}
[semiring R]
(p : (polynomial R)ᵐᵒᵖ) :
(⇑(polynomial.op_ring_equiv R) p).support = (mul_opposite.unop p).support
@[simp]
theorem
polynomial.nat_degree_op_ring_equiv
{R : Type u_1}
[semiring R]
(p : (polynomial R)ᵐᵒᵖ) :
(⇑(polynomial.op_ring_equiv R) p).nat_degree = (mul_opposite.unop p).nat_degree
@[simp]
theorem
polynomial.leading_coeff_op_ring_equiv
{R : Type u_1}
[semiring R]
(p : (polynomial R)ᵐᵒᵖ) :