cycles): is_cycle_of_is_cycle_pow (#6871)

Commit

4 years ago

feat(group_theory/perm/cycles): is_cycle_of_is_cycle_pow (#6871) If `g ^ n` is a cycle, and if `g ^ n` doesn't have smaller support, then `g` is a cycle.

Author

tb65536

Parents

5eead090

mathlib bc33f1a9 - feat(group_theory/perm/cycles): is_cycle_of_is_cycle_pow (#6871)

mathlib
bc33f1a9 - feat(group_theory/perm/cycles): is_cycle_of_is_cycle_pow (#6871)