mathlib

ef7c3350 - fix(data/mv_polynomial): add missing decidable arguments (#7817)

fix(data/mv_polynomial): add missing decidable arguments (#7817) This: * fixes a doubled instance name, `finsupp.finsupp.decidable_eq`. Note the linter deliberate ignores instances, as they are often autogenerated * generalizes `finsupp.decidable_le` to all canonically_ordered_monoids * adds missing `decidable_eq` arguments to `mv_polynomial` and `mv_power_series` lemmas whose statement contains an `if`. These might in future be lintable. * adds some missing lemmas about `mv_polynomial` to clean up a few proofs.