mathlib3

f2984d51 - fix(data/{finsupp,polynomial,mv_polynomial}/basic): add missing decidable arguments (#7309)

fix(data/{finsupp,polynomial,mv_polynomial}/basic): add missing decidable arguments (#7309) Lemmas with an `ite` in their conclusion should not use `classical.dec` or similar, instead inferring an appropriate decidability instance from their context. This eliminates a handful of converts elsewhere. The linter in #6485 should eventually find these automatically.