Commit 2025-01-10 18:59 a5910d1d

View on Github →

feat: s \ t ∩ u = (s ∩ u) \ t (#20298) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Finset/Lattice/Basic.lean

Modified Mathlib/Data/Finset/SDiff.lean

modified theorem Finset.inter_sdiff_assoc

added theorem Finset.inter_sdiff_left_comm

added theorem Finset.sdiff_inter_right_comm

Modified Mathlib/Data/Set/Basic.lean

modified theorem Set.inter_diff_assoc

modified theorem Set.inter_diff_distrib_right

added theorem Set.inter_sdiff_left_comm

added theorem Set.sdiff_inter_right_comm

Modified Mathlib/Order/BooleanAlgebra.lean

modified theorem inf_sdiff_assoc

added theorem inf_sdiff_left_comm

deleted theorem inf_sdiff_right_comm

added theorem sdiff_inf_right_comm