mathlib3

e4da493c - feat(group_theory/perm/sign): exists_pow_eq_of_is_cycle (#5665)

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 Co-authored-by: tb65536 <tb65536@users.noreply.github.com>