Theorem MulAction.nonempty_orbit

Modification history

2025-09-28 19:43
Mathlib/GroupTheory/GroupAction/Defs.lean
feat(Dynamics/Flow): define semiconjugacy, factor and orbit (#28000) …
Added MulAction.nonempty_orbitView on Github →