Theorem Multiset.sub_filter_eq_filter_not

Modification history

2025-02-25 17:02
Mathlib/Data/Multiset/Basic.lean
chore(Data/Multiset): split `Multiset/Basic.lean` into many files (#22126) …
Modified Multiset.sub_filter_eq_filter_notView on Github →
2025-01-06 12:46
Mathlib/Data/Multiset/Basic.lean
chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) …
Modified Multiset.sub_filter_eq_filter_notView on Github →
2024-07-31 23:15
Mathlib/Data/Multiset/Basic.lean
chore: backports for leanprover/lean4#4814 (part 6) (#15313) …
Modified Multiset.sub_filter_eq_filter_notView on Github →
2024-05-25 19:14
Mathlib/Data/Multiset/Basic.lean
feat(Multiset): add two lemmas relating Multiset.filter / Multiset.prod (#9864)
Added Multiset.sub_filter_eq_filter_notView on Github →