Commit 2023-01-19 14:09 1771130d

View on Github →

feat port: Algebra.Module.BigOperators (#1665)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/BigOperators.lean

added theorem Finset.cast_card

added theorem Finset.sum_smul

added theorem Finset.sum_smul_sum

added theorem List.sum_smul

added theorem Multiset.sum_smul

added theorem Multiset.sum_smul_sum