Commit 2021-04-21 19:58 f2984d51

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.