mathlib
65a1391a - feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (#18087)

Commit
2 years ago
feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (#18087) Left commutativity and cardinality of `list.filter`/`multiset.filter`/`finset.filter`. Interaction of `count`/`countp` and `attach`.
Author
Parents
Loading