Commit 2023-05-03 03:14 f69db8ce
View on Github →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.