Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.op_ring_equiv_op_C_mul_X_pow

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_mul_X_powView on Github →