mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

refactor: redefine `Finsupp` as `abbrev` of `DFinsupp`

Open Komyyy opened this issue 1 year ago • 2 comments


  • [ ] depends on: #13025

Open in Gitpod

Komyyy avatar May 15 '24 05:05 Komyyy

This PR/issue depends on:

@digama0 I requested the review for #13025, not this. Sorry.

Komyyy avatar May 19 '24 06:05 Komyyy

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.

Komyyy avatar May 24 '24 02:05 Komyyy