Commit 2023-03-16 06:25 7ff0989c

View on Github →

feat: port RingTheory.Polynomial.Opposites (#2868)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Opposites.lean

added theorem Polynomial.coeff_opRingEquiv

added theorem Polynomial.leadingCoeff_opRingEquiv

added theorem Polynomial.natDegree_opRingEquiv

added def Polynomial.opRingEquiv

added theorem Polynomial.opRingEquiv_op_C

added theorem Polynomial.opRingEquiv_op_C_mul_X_pow

added theorem Polynomial.opRingEquiv_op_X

added theorem Polynomial.opRingEquiv_op_monomial

added theorem Polynomial.opRingEquiv_symm_C

added theorem Polynomial.opRingEquiv_symm_C_mul_X_pow

added theorem Polynomial.opRingEquiv_symm_X

added theorem Polynomial.opRingEquiv_symm_monomial

added theorem Polynomial.support_opRingEquiv