mathlib3

f69db8ce - feat(data/mv_polynomial/basic): add and generalize some lemmas from finsupp and monoid_algebra (#18855)

feat(data/mv_polynomial/basic): add and generalize some lemmas from finsupp and monoid_algebra (#18855) Most of these changes generalize from `distrib_mul_action` to `smul_zero_class`. The new lemmas are all just proved using corresponding lemmas on the underlying types. Co-authored-by: Hagb (Junyu Guo 郭俊余) <hagb_green@qq.com>