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!
Co-authored-by: Johan Commelin <johan@commelin.net>
