Commit 2021-07-28 14:08 0ccd2f66

View on Github →

feat(data/dfinsupp): add simp lemma single_eq_zero (#8447) This matches finsupp.single_eq_zero. Also adds dfinsupp.ext_iff, and changes some lemma arguments to be explicit.

Estimated changes

Modified src/data/dfinsupp.lean

added theorem dfinsupp.ext_iff

modified theorem dfinsupp.single_add

added theorem dfinsupp.single_eq_zero

modified theorem dfinsupp.single_zero