feat(group_theory/perm/basic): Iterating a permutation is the same as…

… taking a power (#13554)

src/group_theory/perm/basic.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import algebra.group.pi
 import algebra.group_power.lemmas
+import logic.function.iterate
 
 /-!
 # The group of permutations (self-equivalences) of a type `α`
@@ -51,10 +52,14 @@ lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y := f.eq_
 
 lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y := f.symm_apply_eq
 
-lemma zpow_apply_comm {α : Type*} (σ : equiv.perm α) (m n : ℤ) {x : α} :
+lemma zpow_apply_comm {α : Type*} (σ : perm α) (m n : ℤ) {x : α} :
   (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x) :=
 by rw [←equiv.perm.mul_apply, ←equiv.perm.mul_apply, zpow_mul_comm]
 
+@[simp] lemma iterate_eq_pow (f : perm α) : ∀ n, f^[n] = ⇑(f ^ n)
+| 0       := rfl
+| (n + 1) := by { rw [function.iterate_succ, pow_add, iterate_eq_pow], refl }
+
 /-! Lemmas about mixing `perm` with `equiv`. Because we have multiple ways to express
 `equiv.refl`, `equiv.symm`, and `equiv.trans`, we want simp lemmas for every combination.
 The assumption made here is that if you're using the group structure, you want to preserve it after