New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore(data/mv_polynomial): use classical logic #1391
Conversation
925f602
to
10580f2
Compare
Sorry, there's still some more files that I missed, so I'm marking this as WIP. |
@jcommelin, @kckennylau, I've run into quite a few problems in |
Thanks! We're down to one remaining problem, described above in the discussion with Mario. |
5da9c1e
to
5792eb1
Compare
…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
Per discussion on Zulip, this PR makes
data/finsupp
,data/polynomial
anddata/mv_polynomial
classical.