Theorem MulAction.orbit.eq_or_disjoint

Modification history

2024-05-28 17:51

Mathlib/GroupTheory/GroupAction/Blocks.lean

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

Added MulAction.orbit.eq_or_disjoint View on Github →