Commit 2023-03-23 23:56 1e1dd61d

View on Github →

chore: put toMultiset into namespace Sym (#2266)

Estimated changes

Modified Mathlib/Data/Sym/Basic.lean

added def Sym.toMultiset

deleted def toMultiset