chore(data/mv_polynomial): use classical logic #1391
ChrisHughes24
merged
46 commits into
master
from
decidable_eq
refactor(linear_algebra/lc): use families not sets
ee5c9f03
refactor(linear_algebra/lc): merge lc into finsupp
9380c31f
refactor(linear_algebra/lc): localize decidability
4b507c80
refactor(linear_algebra/lc): finsupp instances
09780f62
refactor(linear_algebra/lc): use families instead of sets
8a46e26b
refactor(linear_algebra/lc): remove set argument in lin_indep
5fe7c94c
refactor(linear_algebra/lc): clean up
c765545a
refactor(linear_algebra/lc): more clean up
f1a9f1c4
refactor(linear_algebra/lc): set_option in section
b08c1eca
refactor(linear_algebra/lc): decidability proof
c6d57d0d
refactor(linear_algebra/lc): arrow precedence
7314d886
refactor(linear_algebra/lc): more cleanup
e5f9d8ee
make data.finsupp classical
644596f1
trouble with data/polynomial
0e39777f
...
15e417b0
more classical
0b11e84e
merge
3b7a8832
merge
da6f4bb1
merge
ebc9d0d0
merge
a3a800d5
fix
cc29563d
removing more
623a0350
minor
65770743
?
9498841d
progress, using convert
8874d9de
merge
c955bf0f
working?
571e6dd7
remove some unnecessary converts
e4bddfdd
fixes
93fb1686
err
10580f2a
oops
413cb1eb
various
250bf2ff
kim-em
changed the title
various
f72239ca
fix free_comm_ring
547b81e2
remove test lines
2b35c503
fix linear_algebra/matrix.lean
c3e302d6
Merge branch 'master' into decidable_eq
4e4b6242
Fix errors in power_series.lean
dba36f5c
merge master
5b21a1ce
trying to turn instances back on
9c156c43
restore some instances
0a8a0900
Merge branch 'master' into decidable_eq
5792eb11
no joy
c61df7e4
fix mv_polynomial errors
4ef3cb28
another convert
7b78cae0
Merge branch 'master' into decidable_eq
004c0ec9
kim-em
changed the title 
Login to write a write a comment.
Login via GitHub