Commit 2025-01-31 12:56 e58d6d7d

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/Transitive.lean

added theorem MulAction.IsPretransitive.of_surjective_map

added theorem MulAction.isPretransitive_congr

added theorem MulAction.isPretransitive_iff_base

added theorem MulAction.isPretransitive_iff_orbit_eq_top