mathlib
87f8db2e - feat(data/dfinsupp): add coe lemmas (#6343)

Commit

4 years ago

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

Author

eric-wieser

Parents