Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-20 18:42 9d6d8c26

View on Github →

feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554)

Estimated changes

Modified src/group_theory/perm/basic.lean

added theorem equiv.perm.iterate_eq_pow

modified theorem equiv.perm.zpow_apply_comm