mathlib3

79bc6ad4 - feat(data/mv_polynomial/equiv): API for `mv_polynomial.fin_succ_equiv` (#10812)

feat(data/mv_polynomial/equiv): API for `mv_polynomial.fin_succ_equiv` (#10812) This PR provides API for `mv_polynomial.fin_succ_equiv`: coefficients, degree, coefficientes of coefficients, degree_of of coefficients, etc. To state and prove these lemmas I had to define `cons` and `tail` for maps `fin (n+1) →₀ M` and prove the usual properties for these. I'm not sure if this is necessary or the correct approach to do this. Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>