Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-21 21:41 87f8db2e

View on Github →

feat(data/dfinsupp): add coe lemmas (#6343) These lemmas already exist for finsupp, let's add them for dfinsupp too.

Estimated changes

modified theorem dfinsupp.add_apply
added theorem dfinsupp.coe_add
added theorem dfinsupp.coe_neg
added theorem dfinsupp.coe_smul
added theorem dfinsupp.coe_sub
modified theorem dfinsupp.neg_apply
modified theorem dfinsupp.smul_apply
modified theorem dfinsupp.sub_apply