Commit 2024-10-25 07:22 f8829a66

View on Github →

chore: cleanup/split of Data.List.Perm (#18211) Hopefully reduces imports already, and opens the possibility of better splits in Multiset.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Data/List/Dedup.lean

added theorem List.Perm.dedup

Renamed Mathlib/Data/List/Perm.lean to Mathlib/Data/List/Perm/Basic.lean

deleted theorem List.Perm.bagInter

deleted theorem List.Perm.bagInter_left

deleted theorem List.Perm.bagInter_right

deleted theorem List.Perm.dedup

deleted theorem List.Perm.dropSlice_inter

deleted theorem List.Perm.drop_inter

deleted theorem List.Perm.inter_append

deleted theorem List.Perm.take_inter

deleted theorem List.cons_subperm_of_mem

modified theorem List.perm_replicate_append_replicate

deleted theorem List.subperm_cons_self

deleted theorem List.subperm_iff

deleted theorem List.subperm_singleton_iff

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

added theorem List.Perm.bagInter

added theorem List.Perm.bagInter_left

added theorem List.Perm.bagInter_right

added theorem List.Perm.dropSlice_inter

added theorem List.Perm.drop_inter

added theorem List.Perm.inter_append

added theorem List.Perm.take_inter

Created Mathlib/Data/List/Perm/Subperm.lean

added theorem List.cons_subperm_of_mem

added theorem List.subperm_cons_self

added theorem List.subperm_iff

added theorem List.subperm_singleton_iff

Modified Mathlib/Data/List/Permutation.lean

Modified Mathlib/Data/List/Prime.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Multiset/Dedup.lean

Modified Mathlib/Data/Nat/Factors.lean

Modified test/MkIffOfInductive.lean