[Merged by Bors] - feat(Data/Fintype/List): generalize fintypeNodupList (no DecidableEq)#16656
Closed
mo271 wants to merge 13 commits intomasterfrom mo271/improve_fintypeNodupList
+69-23
Commits
Commits on Sep 10, 2024
Commits on Sep 12, 2024
Commits on Nov 12, 2024
Commits on Dec 1, 2024
- committed
Commits on Dec 2, 2024
Commits on Jan 14, 2025
- committed
- committed
- committed
- committed
- committed