Def Multiset.toFinsupp

Modification history

2026-09-10 11:06
Mathlib/Data/Finsupp/Multiset.lean
fix: `macro_inline` `DFunLike` instances to make `Multiset.toFinsupp` computable (#43620) …
Added Multiset.toFinsuppView on Github →
2026-02-24 10:38
Mathlib/Data/Finsupp/Multiset.lean
chore: bump toolchain to v4.29.0-rc2 (#35708)
Deleted Multiset.toFinsuppView on Github →
2023-08-07 12:37
Mathlib/Data/Finsupp/Multiset.lean
feat(Data/Finsupp): make toMultiset and antidiagonal computable (#6331) …
Modified Multiset.toFinsuppView on Github →
2023-02-03 18:59
Mathlib/Data/Finsupp/Multiset.lean
feat: port Data.Finsupp.Multiset (#1988) …
Added Multiset.toFinsuppView on Github →