Commit 2025-03-31 11:38 39afc301

View on Github →

refactor(Data): split off material on Set.Pairwise from List.Nodup (#23407) Importing Data.Set.Pairwise in Data.List.Nodup comes with quite a bit of transitive dependencies, including on the long pole. I tried reversing the import direction, but going the other way lead to a lot more transitive imports. So let's split the files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Pairwise.lean

Modified Mathlib/Data/List/Dedup.lean

Modified Mathlib/Data/List/Nodup.lean

deleted theorem List.Nodup.pairwise_coe

deleted theorem List.Nodup.pairwise_of_set_pairwise

Modified Mathlib/Data/List/Perm/Lattice.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/Multiset/Filter.lean

Modified Mathlib/Data/Multiset/UnionInter.lean

Modified Mathlib/Data/Prod/TProd.lean

Created Mathlib/Data/Set/Pairwise/List.lean

added theorem List.Nodup.pairwise_coe

added theorem List.Nodup.pairwise_of_set_pairwise

Modified scripts/noshake.json