mathlib3

[Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances

#19187

Closed