Theorem MulAction.oneEmbedding_isPretransitive_iff

Modification history

2025-05-18 18:58
Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean
feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions (#23386) …
Added MulAction.oneEmbedding_isPretransitive_iffView on Github →