Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-19 06:12 f2c162c1

View on Github →

feat(data/dfinsupp): more lemmas about erase, filter, and negation (#9248)

Estimated changes

Modified src/data/dfinsupp.lean

added theorem dfinsupp.erase_add

added def dfinsupp.erase_add_hom

added theorem dfinsupp.erase_neg

added theorem dfinsupp.erase_single

added theorem dfinsupp.erase_single_ne

added theorem dfinsupp.erase_single_same

added theorem dfinsupp.erase_sub

added theorem dfinsupp.erase_zero

added theorem dfinsupp.filter_single

added theorem dfinsupp.filter_single_neg

added theorem dfinsupp.filter_single_pos

added theorem dfinsupp.single_neg

added theorem dfinsupp.single_sub