mathlib
4ae8752c - chore(data/mv_polynomial): use bundled homs (#3595)

Commit
5 years ago
chore(data/mv_polynomial): use bundled homs (#3595) I've done a lot of the scut work, but there are still about half a dozen broken proofs, if anyone would like to take a bash at them! Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading