Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-16 19:28 d4fda045

View on Github →

feat(data/finsupp/basic): add a few lemmas, mostly about finsupp.filter (#13457)

Estimated changes

Modified src/data/finsupp/basic.lean

added theorem finsupp.filter_eq_self_iff

added theorem finsupp.filter_eq_zero_iff

modified theorem finsupp.filter_single_of_neg

modified theorem finsupp.filter_single_of_pos

added theorem finsupp.prod_div_prod_filter

added theorem finsupp.prod_filter_index

added theorem finsupp.prod_filter_mul_prod_filter_not

added theorem finsupp.single_apply_ne_zero