Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-27 03:05 bc33f1a9

View on Github →

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.

Estimated changes