mathlib3

b4cad379 - chore(ring_theory/mv_polynomial/basic): golf (#13765)