Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-26 14:18 ba5594a6

View on Github →

feat(data/dfinsupp): Add missing to_additive lemmas (#4788)

Estimated changes

Modified src/data/dfinsupp.lean

added theorem dfinsupp.prod_inv

added theorem dfinsupp.prod_mul

added theorem dfinsupp.prod_one

deleted theorem dfinsupp.sum_add

deleted theorem dfinsupp.sum_neg

deleted theorem dfinsupp.sum_zero