Theorem MulAction.IsBlock.of_orbit

Modification history

2024-07-11 10:12
Mathlib/GroupTheory/GroupAction/Blocks.lean
feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups (#13995) …
Added MulAction.IsBlock.of_orbitView on Github →