Commit 2023-02-01 17:23 c59116f1

View on Github →

feat : port Data.Finsupp.BigOperators (#1982)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/BigOperators.lean

added theorem Finset.mem_sup_support_iff

added theorem Finset.support_sum_eq

added theorem Finset.support_sum_subset

added theorem List.mem_foldr_sup_support_iff

added theorem List.support_sum_eq

added theorem List.support_sum_subset

added theorem Multiset.mem_sup_map_support_iff

added theorem Multiset.support_sum_eq

added theorem Multiset.support_sum_subset