chore(data/mv_polynomial): use classical logic (#1391)
* refactor(linear_algebra/lc): use families not sets
* refactor(linear_algebra/lc): merge lc into finsupp
* refactor(linear_algebra/lc): localize decidability
* refactor(linear_algebra/lc): finsupp instances
* refactor(linear_algebra/lc): use families instead of sets
* refactor(linear_algebra/lc): remove set argument in lin_indep
* refactor(linear_algebra/lc): clean up
* refactor(linear_algebra/lc): more clean up
* refactor(linear_algebra/lc): set_option in section
* refactor(linear_algebra/lc): decidability proof
* refactor(linear_algebra/lc): arrow precedence
* refactor(linear_algebra/lc): more cleanup
* make data.finsupp classical
* trouble with data/polynomial
* ...
* more classical
* merge
* merge
* merge
* fix
* removing more
* minor
* ?
* progress, using convert
* working?
* remove some unnecessary converts
* fixes
* err
* oops
* various
* various
* fix free_comm_ring
* remove test lines
* fix linear_algebra/matrix.lean
* Fix errors in power_series.lean
* trying to turn instances back on
* restore some instances
* no joy
* fix mv_polynomial errors
* another convert
