Commit 2022-04-10 09:05 c916b64d

View on Github →

feat(ring_theory/polynomial/opposites + data/{polynomial/basic + finsupp/basic}): move op_ring_equiv to a new file + lemmas (#13162) This PR moves the isomorphism R[X]ᵐᵒᵖ ≃+* Rᵐᵒᵖ[X] to a new file ring_theory.polynomial.opposites. I also proved some basic lemmas about the equivalence. Zulip discussion

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.support_map_range_of_injective

Modified src/data/polynomial/basic.lean

deleted def polynomial.op_ring_equiv

Created src/ring_theory/polynomial/opposites.lean

added theorem polynomial.coeff_op_ring_equiv

added theorem polynomial.leading_coeff_op_ring_equiv

added theorem polynomial.nat_degree_op_ring_equiv

added def polynomial.op_ring_equiv

added theorem polynomial.op_ring_equiv_op_C

added theorem polynomial.op_ring_equiv_op_C_mul_X_pow

added theorem polynomial.op_ring_equiv_op_X

added theorem polynomial.op_ring_equiv_op_monomial

added theorem polynomial.op_ring_equiv_symm_C

added theorem polynomial.op_ring_equiv_symm_C_mul_X_pow

added theorem polynomial.op_ring_equiv_symm_X

added theorem polynomial.op_ring_equiv_symm_monomial

added theorem polynomial.support_op_ring_equiv