feat(data/mv_polynomial): fill in API for vars (#4018)
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 <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>



Co-authored-by: Johan Commelin <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib