mathlib3 documentation

ring_theory.polynomial.opposites

Interactions between R[X] and Rᵐᵒᵖ[X] #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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.

Equations

Lemmas to get started, using op_ring_equiv R on the various expressions of finsupp.single: monomial, C a, X, C a * X ^ n.

source
@[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)
source
@[simp]
theorem polynomial.op_ring_equiv_op_C {R : Type u_1} [semiring R] (a : R) :
⇑(polynomial.op_ring_equiv R) (mul_opposite.op (⇑polynomial.C a)) = ⇑polynomial.C (mul_opposite.op a)
source
@[simp]
theorem polynomial.op_ring_equiv_op_X {R : Type u_1} [semiring R] :
⇑(polynomial.op_ring_equiv R) (mul_opposite.op polynomial.X) = polynomial.X
source
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.

source
@[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))
source
@[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))
source
@[simp]
theorem polynomial.op_ring_equiv_symm_X {R : Type u_1} [semiring R] :
⇑((polynomial.op_ring_equiv R).symm) polynomial.X = mul_opposite.op polynomial.X
source
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.

source
@[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)
source
@[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
source
@[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
source
@[simp]
theorem polynomial.leading_coeff_op_ring_equiv {R : Type u_1} [semiring R] (p : (polynomial R)ᵐᵒᵖ) :
(⇑(polynomial.op_ring_equiv R) p).leading_coeff = mul_opposite.op (mul_opposite.unop p).leading_coeff