Commit 2024-05-25 19:14 4d5bca96

View on Github →

feat(Multiset): add two lemmas relating Multiset.filter / Multiset.prod (#9864)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Multiset.lean

added theorem Multiset.prod_filter_mul_prod_filter_not

Modified Mathlib/Data/Multiset/Basic.lean

added theorem Multiset.sub_filter_eq_filter_not