mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(data/finsupp/equiv_dfinsupp): add an equivalence between finsupp and dfinsupp

Open eric-wieser opened this issue 4 years ago • 1 comments

Doing this for subgroup is slightly harder as some simp lemmas are missing - so I will leave that to a follow up.

  • [x] depends on: #7311

Open in Gitpod

The missing simp lemma that would be needed for subgroups is in #7218

eric-wieser avatar Apr 16 '21 08:04 eric-wieser

This PR/issue depends on:

  • ~~leanprover-community/mathlib#7311~~ By Dependent Issues (🤖). Happy coding!

github-actions[bot] avatar Dec 25 '21 12:12 github-actions[bot]