Commit 2024-10-18 21:00 547e8787

View on Github →

feat: Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t) (#17907)

Estimated changes

Modified Mathlib/Data/Set/Pointwise/SMul.lean

added theorem Set.disjoint_smul_set

added theorem Set.disjoint_smul_set_left

added theorem Set.disjoint_smul_set_right

deleted theorem Set.smul_set_disjoint_iff

modified theorem Set.smul_set_iInter