Commit 2021-01-16 00:47 e4da493c
View on Github →feat(group_theory/perm/sign): exists_pow_eq_of_is_cycle (#5665)
Slight generalization of exists_gpow_eq_of_is_cycle in the case of a cycle on a finite set.
Also move the following from group_theory/perm/sign.lean to group_theory/perm/cycles.lean:
- is_cycle
- is_cycle_swap
- is_cycle_inv
- exists_gpow_eq_of_is_cycle
- is_cycle_swap_mul_aux₁
- is_cycle_swap_mul_aux₂
- eq_swap_of_is_cycle_of_apply_apply_eq_self
- is_cycle_swap_mul
- sign_cycle