mathlib3

c916b64d - feat(ring_theory/polynomial/opposites + data/{polynomial/basic + finsupp/basic}): move `op_ring_equiv` to a new file + lemmas (#13162)

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](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members)