mathlib4
mathlib4 copied to clipboard
refactor: redefine `Finsupp` as `abbrev` of `DFinsupp`
This PR/issue depends on:
- leanprover-community/mathlib4#13025 By Dependent Issues (🤖). Happy coding!
@digama0 I requested the review for #13025, not this. Sorry.
I abort this task because it's a hard work and I have no times to do currenlty. Maybe I restart this task later so I restore this branch.