mathlib

ae72826a - feat(data/mv_polynomial): define comap (#4161)

feat(data/mv_polynomial): define comap (#4161) More from the Witt vector branch. Co-authored by: Johan Commelin <johan@commelin.net> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>