mathlib

2f5b500a - fix(data/mv_polynomial): add missing `decidable_eq` arguments to lemmas (#18848)

fix(data/mv_polynomial): add missing `decidable_eq` arguments to lemmas (#18848) This does not change the type of any definitions; the effect of this PR is to make the *statement* of the lemmas syntactically more general. To ensure this catches them all, this removes `open_locale classical` from the beginning of every file in `data/mv_polynomial` and `ring_theory/mv_polynomial`. For definitions which bake in a `classical.dec_eq` assumption, this adds a lemma proven by `convert rfl` that unfolds them to a version with an arbitrary `decidable_eq` instance, following a pattern established elsewhere. Unlike previous refactors of this style this doesn't seemed to have helped any downstream proofs much.