Commit 2025-03-04 07:48 b6520862
View on Github →chore(Data/Multiset): redistribute Nodup material (#22502)
Now that Multiset.Nodup lives in Multiset/Defs.lean, all the material on Nodup in Nodup.lean can be upstreamed to other files in the Multiset folder. We are left with Pairwise.forall which doesn't mention Nodup at all, so I renamed the file to Pairwise.lean. (Note that Git decided it is a deletion + addition, not a rename...)
Source of the Pairwise.lean attribution: https://github.com/leanprover-community/mathlib3/pull/569