mathlib3
62963861 - feat(data/mv_polynomial): fill in API for vars (#4018)

Commit
5 years ago
feat(data/mv_polynomial): fill in API for vars (#4018) `mv_polynomial.vars` was missing a lot of API. This doesn't cover everything, but it fleshes out the theory quite a bit. There's probably more coming eventually -- this is what we have now. Co-authored by: Johan Commelin <johan@commelin.net> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading