Theorem MulAction.pow_smul_ne_of_lt_period

Modification history

2024-02-15 13:05
Mathlib/GroupTheory/GroupAction/Period.lean
feat(GroupTheory/GroupAction): define MulAction.period and create GroupTheory/GroupAction/Period (#9490) …
Added MulAction.pow_smul_ne_of_lt_periodView on Github →