Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-05 14:19 92b9a00d

View on Github →

feat(data/finsupp): to_/of_multiset, curry/uncurry

Estimated changes

Modified data/finset.lean

added theorem finset.mem_subtype

Modified data/finsupp.lean

deleted theorem finset.mem_subtype

added theorem finsupp.count_to_multiset

added def finsupp.equiv_multiset

added def finsupp.finsupp_prod_equiv

modified theorem finsupp.map_domain_finset_sum

added theorem finsupp.mem_support_finset_sum

added theorem finsupp.mem_support_multiset_sum

added theorem finsupp.mem_support_single

added def finsupp.of_multiset

added theorem finsupp.of_multiset_apply

modified theorem finsupp.prod_add_index

modified theorem finsupp.prod_finset_sum_index

modified theorem finsupp.prod_map_domain_index

modified theorem finsupp.prod_sum_index

added theorem finsupp.single_finset_sum

added theorem finsupp.single_multiset_sum

added theorem finsupp.single_sum

modified theorem finsupp.sum_add

added theorem finsupp.sum_curry_index

modified theorem finsupp.sum_neg

modified theorem finsupp.sum_sub_index

modified theorem finsupp.sum_zero

added def finsupp.to_multiset

modified structure finsupp