Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-17 20:09 c42a9ad1

View on Github →

chore(data/finsupp/basic): lemmas about sub and neg on filter and erase (#9228)

Estimated changes

Modified src/data/finsupp/basic.lean

added def finsupp.erase_add_hom

added theorem finsupp.erase_neg

added theorem finsupp.erase_sub

added theorem finsupp.filter_neg

added theorem finsupp.filter_sub