!4#3225 porting MvPolynomial.Funext

Stream: mathlib4

[Scott Morrison]

In !4#3225 I rewrote a timing-out proof, by writing some missing lemmas about eval₂. If anyone would like to backport these to mathlib3 (moved to their correct homes) that would be amazing. If no one picks up on it I will get there eventually. :-)

[Jason Yuen]

It looks like !4#3225 ports data.mv_polynomial.polynomial. However, the porting status page didn't know this file was ported.
https://leanprover-community.github.io/mathlib-port-status/file/data/mv_polynomial/polynomial

[Scott Morrison]

The problem is that !4#3225 created the file Mathlib.Data.MvPolynomial.Polynomial before the corresponding file even existed in mathlib3. It was then backported. That, however, means that it is missing the header it should have.

[Scott Morrison]

The remaining porting obligation is just to add that header!

[Jason Yuen]

I made an attempt at !4#3723