Commit 2023-05-14 22:21 2f5b500a

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.