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

Estimated changes

deleted theorem Multiset.Nodup.add_iff
deleted theorem Multiset.Nodup.cons
deleted theorem Multiset.Nodup.erase
deleted theorem Multiset.Nodup.filter
deleted theorem Multiset.Nodup.inter_left
deleted theorem Multiset.Nodup.map
deleted theorem Multiset.Nodup.map_on
deleted theorem Multiset.Nodup.not_mem
deleted theorem Multiset.Nodup.of_cons
deleted theorem Multiset.Nodup.of_map
deleted theorem Multiset.Nodup.pmap
deleted theorem Multiset.Pairwise.forall
deleted theorem Multiset.mem_sub_of_nodup
deleted theorem Multiset.nodup_add
deleted theorem Multiset.nodup_attach
deleted theorem Multiset.nodup_cons
deleted theorem Multiset.nodup_iff_le
deleted theorem Multiset.nodup_of_le
deleted theorem Multiset.nodup_range
deleted theorem Multiset.nodup_singleton
deleted theorem Multiset.nodup_union
deleted theorem Multiset.nodup_zero
deleted theorem Multiset.not_nodup_pair
deleted theorem Multiset.range_le