Commit 2024-02-19 21:18 43b77bb9

View on Github →

feat: smul_set_disjoint_iff (#10703) Add a simp lemma about the group action on a set: Disjoint (a • s) (a • t) ↔ Disjoint s t. From AperiodicMonotilesLean.

Estimated changes

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

added theorem Set.smul_set_disjoint_iff