Commit 2025-03-12 12:49 2cf5be16
View on Github →chore(Data/Multiset): clean up porting notes (#22835) A lot of porting notes are about definitions working slightly differently in Lean 4. We seem to be happy with the current setup so just drop these.