Commit 2020-10-02 20:49 da24addb

View on Github →

feat(data/multiset): ordered sum lemmas (#4305) Add some lemmas about products in ordered monoids and sums in ordered add monoids, and a multiset count filter lemma (and a rename of a count filter lemma)

Estimated changes

Modified src/data/list/basic.lean

added theorem list.all_one_of_le_one_le_of_prod_eq_one

added theorem list.one_le_prod_of_one_le

added theorem list.single_le_prod

added theorem list.sum_eq_zero_iff

Modified src/data/multiset/basic.lean

added theorem multiset.all_one_of_le_one_le_of_prod_eq_one

deleted theorem multiset.count_filter

added theorem multiset.count_filter_of_neg

added theorem multiset.count_filter_of_pos

added theorem multiset.one_le_prod_of_one_le

added theorem multiset.single_le_prod

added theorem multiset.sum_eq_zero_iff