Commit 2023-11-08 22:44 92d78f80

View on Github →

feat: attach and filter lemmas (#1470) Match https://github.com/leanprover-community/mathlib/pull/18087

Estimated changes

added theorem Finset.card_filter
added theorem Finset.prod_map_val
modified theorem Finset.sum_boole
added theorem Finset.card_val
added theorem Finset.filter_attach'
added theorem Finset.filter_attach
added theorem Finset.map_filter'
added theorem List.attach_nil
added theorem List.filter_attach'
added theorem List.filter_attach
added theorem List.filter_comm
added theorem List.map_filter'
added theorem List.countP_attach
added theorem List.count_attach
added theorem Multiset.countP_attach
added theorem Multiset.count_attach
added theorem Multiset.filter_attach
added theorem Multiset.filter_comm
added theorem Multiset.map_filter'