Theorem MulAction.isPreprimitive_of_is_two_pretransitive

Modification history

2025-05-18 18:58

Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions (#23386) …

Added MulAction.isPreprimitive_of_is_two_pretransitive View on Github →