Theorem MulAction.IsPretransitive.of_surjective_map

Modification history

2025-01-31 12:56

Mathlib/GroupTheory/GroupAction/Transitive.lean

feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285)

Added MulAction.IsPretransitive.of_surjective_map View on Github →