mathlib3

9eb341a1 - feat(mv_polynomial): minor simplification in coeff_mul (#4586)

feat(mv_polynomial): minor simplification in coeff_mul (#4586) The proof was already golfed in #4472. Use `×` instead of `sigma`. Shorten one line over 100 chars.