Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.leading_coeff_op_ring_equiv

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.leading_coeff_op_ring_equivView on Github →