feat(data/mv_polynomial): assorted lemmas (#4002)
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 <759412786bc533369b22377bf83fb9056c5b25b2@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 <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib