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.

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

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) : (opRingEquiv R) (MulOpposite.op ((monomial n) r)) = (monomial n) (MulOpposite.op r)

@[simp]

theorem Polynomial.opRingEquiv_op_C {R : Type u_1} [Semiring R] (a : R) : (opRingEquiv R) (MulOpposite.op (C a)) = C (MulOpposite.op a)

@[simp]

theorem Polynomial.opRingEquiv_op_X {R : Type u_1} [Semiring R] : (opRingEquiv R) (MulOpposite.op X) = X

theorem Polynomial.opRingEquiv_op_C_mul_X_pow {R : Type u_1} [Semiring R] (r : R) (n : ℕ) : (opRingEquiv R) (MulOpposite.op (C r * X ^ n)) = C (MulOpposite.op r) * 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ᵐᵒᵖ) : (opRingEquiv R).symm ((monomial n) r) = MulOpposite.op ((monomial n) (MulOpposite.unop r))

@[simp]

theorem Polynomial.opRingEquiv_symm_C {R : Type u_1} [Semiring R] (a : Rᵐᵒᵖ) : (opRingEquiv R).symm (C a) = MulOpposite.op (C (MulOpposite.unop a))

@[simp]

theorem Polynomial.opRingEquiv_symm_X {R : Type u_1} [Semiring R] : (opRingEquiv R).symm X = MulOpposite.op X

theorem Polynomial.opRingEquiv_symm_C_mul_X_pow {R : Type u_1} [Semiring R] (r : Rᵐᵒᵖ) (n : ℕ) : (opRingEquiv R).symm (C r * X ^ n) = MulOpposite.op (C (MulOpposite.unop r) * 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 : ℕ) : ((opRingEquiv R) p).coeff n = MulOpposite.op ((MulOpposite.unop p).coeff n)

@[simp]

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

@[simp]

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

@[simp]

theorem Polynomial.leadingCoeff_opRingEquiv {R : Type u_1} [Semiring R] (p : (Polynomial R)ᵐᵒᵖ) : ((opRingEquiv R) p).leadingCoeff = MulOpposite.op (MulOpposite.unop p).leadingCoeff

theorem Polynomial.isLeftCancelMulZero_iff {R : Type u_1} [Semiring R] : IsLeftCancelMulZero (Polynomial R) ↔ IsLeftCancelMulZero R ∧ IsCancelAdd R

theorem Polynomial.isRightCancelMulZero_iff {R : Type u_1} [Semiring R] : IsRightCancelMulZero (Polynomial R) ↔ IsRightCancelMulZero R ∧ IsCancelAdd R

theorem Polynomial.isCancelMulZero_iff {R : Type u_1} [Semiring R] : IsCancelMulZero (Polynomial R) ↔ IsCancelMulZero R ∧ IsCancelAdd R

theorem Polynomial.isDomain_iff {R : Type u_1} [Semiring R] : IsDomain (Polynomial R) ↔ IsDomain R ∧ IsCancelAdd R