Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-05 14:33 3a3249ea

View on Github →

feat(data/finsupp): multiset_map_sum/_sum_sum/_index

Estimated changes

Modified data/finsupp.lean

modified theorem finsupp.map_domain_finset_sum

added theorem finsupp.multiset_map_sum

added theorem finsupp.multiset_sum_sum

added theorem finsupp.multiset_sum_sum_index

modified theorem finsupp.prod_finset_sum_index

modified theorem finsupp.prod_single