mathlib

ab155ef9 - refactor(*): refactor `sum_smul`/`smul_sum` (#1910)

refactor(*): refactor `sum_smul`/`smul_sum` (#1910) * refactor(*): refactor `sum_smul`/`smul_sum` API changes: * Define both versions for `list, `multiset`, and `finset`; * new `finset.smul_sum` is the old `finset.smul_sum` or `_root_.sum_smul.symm`` * new `finset.sum_smul` is the old `finset.smul_sum'` * new `smul_smul` doesn't need a `Type` argument * some lemmas are generalized to a `semimodule` or a `distrib_mul_action` * Fix compile