Theorems · Definition · ring theory
Polynomial.opRingEquiv
(R : Type u_2) → [inst : 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.
- Defined in
- Mathlib.RingTheory.Polynomial.Opposites
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Polynomialstatement · cited by 5,681
- RingEquivstatement · cited by 1,147
- MulOppositestatement and proof · cited by 1,135
- RingEquiv.symmproof · cited by 567
- AddEquiv.symmproof · cited by 530
- RingEquiv.transproof · cited by 54
- Polynomial.toFinsuppIsoproof · cited by 11
- AddMonoidAlgebra.mapDomainRingEquivproof · cited by 8
- RingEquiv.opproof · cited by 7
- AddMonoidAlgebra.opRingEquivproof · cited by 6
Cited by13
Results whose statement or proof uses this declaration.
- Polynomial.opRingEquiv_op_monomialstatement · cited by 3
- Polynomial.opRingEquiv_symm_monomialstatement and proof · cited by 3
- Polynomial.coeff_opRingEquivstatement · cited by 2
- Polynomial.opRingEquiv_op_Cstatement · cited by 1
- Polynomial.natDegree_opRingEquivstatement and proof · cited by 1
- Polynomial.opRingEquiv_op_Xstatement · cited by 1
- Polynomial.support_opRingEquivstatement · cited by 1
- Polynomial.isRightCancelMulZero_iffproof · cited by 0
- Polynomial.opRingEquiv_op_C_mul_X_powstatement and proof · cited by 0
- Polynomial.opRingEquiv_symm_Cstatement · cited by 0
- Polynomial.opRingEquiv_symm_C_mul_X_powstatement and proof · cited by 0
- Polynomial.opRingEquiv_symm_Xstatement · cited by 0