Commit 2023-08-07 12:37 758fc17d

feat(Data/Finsupp): make toMultiset and antidiagonal computable (#6331) In Lean 3, the computability of Finsupp.toMultiset was poisoned by the AddMonoid (α →₀ ℕ) instance, even though this was not used in computation. This is no longer the case in Lean 4, so we can make this computable by adding a DecidableEq α argument. We loosely follow the pattern used with DFinsupp, where we split the declaration in two, as only one direction needs DecidableEq α. As a result, Finsupp.toMultiset is now only an AddMonoidHom, though Multiset.toFinset remains an equiv. We're missing some of the formatting infrastructure for this to be pretty, but this now works:

#eval ((Finsupp.mk Finset.univ ![1, 2, 3] sorry).antidiagonal).image
  fun x : _ × _ => (x.1.toFun, x.2.toFun)