Theorem Set.smul_set_iInter

Modification history

2024-10-18 21:00

Mathlib/Data/Set/Pointwise/SMul.lean

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

Modified Set.smul_set_iInter View on Github →

2024-05-28 17:51

Mathlib/Data/Set/Pointwise/SMul.lean

Feat (GroupTheory/GroupAction/Blocks) : blocks for a mul action (#12049) …

Added Set.smul_set_iInter View on Github →