Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-13 05:13 3185c251

View on Github →

feat(data/list/{count,perm},data/multiset/basic): countp and count lemmas (#14108)

Estimated changes

Modified src/data/list/count.lean

added theorem list.count_eq_zero

added theorem list.countp_cons

added theorem list.countp_eq_zero

Modified src/data/list/perm.lean

added theorem list.countp_eq_countp_filter_add

added theorem list.filter_append_perm

added theorem list.perm.countp_congr

Modified src/data/multiset/basic.lean

added theorem multiset.card_eq_countp_add_countp

added theorem multiset.count_eq_card

added theorem multiset.count_le_card

added theorem multiset.countp_congr

added theorem multiset.countp_eq_card

added theorem multiset.countp_eq_countp_filter_add

added theorem multiset.countp_eq_zero

added theorem multiset.countp_false

added theorem multiset.countp_le_card

added theorem multiset.countp_true