refactor(data/mv_polynomial): split into multiple files (#4070)
`mv_polynomial.lean` was getting massive and hard to explore. This breaks it into (somewhat arbitrary) pieces. While `basic.lean` is still fairly long, there are a lot of basics about multivariate polynomials, and I think it's reasonable.
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
