Commit 2020-09-09 08:45 77c8415b

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.