mathlib3

1d1a0415 - chore(data/mv_polynomial/basic): coeff_mul, more golfing and speedup (#4472)