Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.op_ring_equiv_op_C

Modification history

2022-04-10 09:05

src/ring_theory/polynomial/opposites.lean

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

Added polynomial.op_ring_equiv_op_C View on Github →