Commit 2020-09-01 09:54 a97d71b5

feat(data/mv_polynomial): assorted lemmas (#4002) Assorted additions to mv_polynomial. This is more from the Witt vector development. Nothing too deep here, just scattered lemmas and the constant_coeff ring hom. Coauthored by: Johan Commelin johan@commelin.net

<!-- put comments you want to keep out of the PR commit here -->

Hopefully this builds -- it's split off from a branch with a lot of other changes. I think it shouldn't have dependencies!