Commit 2024-10-28 06:12 deda35aa

View on Github →

chore: split Data.Set.Basic (#18317) Delay imports of Data.Order.SymmDiff, as many things downstream don't need it.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Center.lean

Modified Mathlib/Algebra/Group/Indicator.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/PEquiv.lean

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/Data/Set/Basic.lean

deleted theorem Set.inter_symmDiff_distrib_left

deleted theorem Set.inter_symmDiff_distrib_right

deleted theorem Set.mem_symmDiff

deleted theorem Set.subset_symmDiff_union_symmDiff_left

deleted theorem Set.subset_symmDiff_union_symmDiff_right

deleted theorem Set.symmDiff_eq_empty

deleted theorem Set.symmDiff_nonempty

deleted theorem Set.symmDiff_subset_union

Modified Mathlib/Data/Set/Enumerate.lean

Modified Mathlib/Data/Set/Image.lean

Created Mathlib/Data/Set/SymmDiff.lean

added theorem Set.inter_symmDiff_distrib_left

added theorem Set.inter_symmDiff_distrib_right

added theorem Set.mem_symmDiff

added theorem Set.subset_symmDiff_union_symmDiff_left

added theorem Set.subset_symmDiff_union_symmDiff_right

added theorem Set.symmDiff_eq_empty

added theorem Set.symmDiff_nonempty

added theorem Set.symmDiff_subset_union

Modified Mathlib/Data/SetLike/Basic.lean

Modified Mathlib/Order/Filter/Defs.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

Modified Mathlib/Topology/Connected/Basic.lean

Modified scripts/noshake.json