mathlib3

fa9d2bf3 - feat(data/mv_polynomial/variables): add mv_polynomial.total_deg_finset_sum (#11375)

feat(data/mv_polynomial/variables): add mv_polynomial.total_deg_finset_sum (#11375) Total degree of a sum of mv_polynomials is less than or equal to the maximum of all their degrees. Co-authored-by: jlh <48520973+Jlh18@users.noreply.github.com>