mathlib3

bbfeff38 - feat(data/mv_polynomial/monad): mv_polynomial is a monad in two different ways (#4080)

feat(data/mv_polynomial/monad): mv_polynomial is a monad in two different ways (#4080) These definitions and lemmas significantly decrease the pain in several computations in the Witt project. Co-authored-by: Robert Y. Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>