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