refactor(group_theory/perm/basic): Redefine pow in terms of iterate

src/algebra/hom/iterate.lean

@@ -21,6 +21,10 @@ So, we restate standard `*_hom.map_*` lemmas under names `*_hom.iterate_map_*`.
 
 We also prove formulas for iterates of add/mul left/right.
 
+## TODO
+
+Redefine `npow` in `monoid_hom.End`, `module.End`, etc using `nat.iterate`.
+
 ## Tags
 
 homomorphism, iterate

src/dynamics/fixed_points/basic.lean

@@ -86,8 +86,7 @@ h.to_left_inverse e.left_inverse_symm
 
 protected lemma perm_inv (h : is_fixed_pt e x) : is_fixed_pt ⇑(e⁻¹) x := h.equiv_symm
 
-protected lemma perm_pow (h : is_fixed_pt e x) (n : ℕ) : is_fixed_pt ⇑(e ^ n) x :=
-by { rw equiv.perm.coe_pow, exact h.iterate _ }
+protected lemma perm_pow (h : is_fixed_pt e x) (n : ℕ) : is_fixed_pt ⇑(e ^ n) x := h.iterate _
 
 protected lemma perm_zpow (h : is_fixed_pt e x) : ∀ n : ℤ, is_fixed_pt ⇑(e ^ n) x
 | (int.of_nat n) := h.perm_pow _

src/group_theory/group_action/defs.lean

@@ -8,6 +8,7 @@ import algebra.group.commute
 import algebra.hom.group
 import algebra.opposites
 import logic.embedding.basic
+import logic.function.iterate
 
 /-!
 # Definitions of group actions
@@ -844,7 +845,9 @@ instance : monoid (function.End α) :=
   mul := (∘),
   mul_assoc := λ f g h, rfl,
   mul_one := λ f, rfl,
-  one_mul := λ f, rfl, }
+  one_mul := λ f, rfl,
+  npow := λ n f, f^[n],
+  npow_succ' := λ n f, function.iterate_succ' _ _ }
 
 instance : inhabited (function.End α) := ⟨1⟩
 

src/group_theory/perm/basic.lean

@@ -31,7 +31,15 @@ instance perm_group : group (perm α) :=
   mul_assoc := λ f g h, (trans_assoc _ _ _).symm,
   one_mul := trans_refl,
   mul_one := refl_trans,
-  mul_left_inv := self_trans_symm }
+  mul_left_inv := self_trans_symm,
+  npow := λ n f, ⟨f^[n], f.symm^[n], f.left_inv.iterate _, f.right_inv.iterate _⟩,
+  npow_succ' := λ n f, coe_fn_injective $ function.iterate_succ' _ _,
+  zpow := λ n, match n with
+  | int.of_nat n := λ f, ⟨f^[n], f.symm^[n], f.left_inv.iterate _, f.right_inv.iterate _⟩
+  | int.neg_succ_of_nat n := λ f,
+      ⟨f.symm^[n + 1], f^[n + 1], f.right_inv.iterate _, f.left_inv.iterate _⟩
+  end,
+  zpow_succ' := λ n f, coe_fn_injective $ function.iterate_succ' _ _ }
 
 @[simp] lemma default_eq : (default : perm α) = 1 := rfl
 
@@ -68,9 +76,8 @@ lemma inv_def (f : perm α) : f⁻¹ = f.symm := rfl
 
 @[simp, norm_cast] lemma coe_one : ⇑(1 : perm α) = id := rfl
 @[simp, norm_cast] lemma coe_mul (f g : perm α) : ⇑(f * g) = f ∘ g := rfl
-@[norm_cast] lemma coe_pow (f : perm α) (n : ℕ) : ⇑(f ^ n) = (f^[n]) :=
-hom_coe_pow _ rfl (λ _ _, rfl) _ _
-@[simp] lemma iterate_eq_pow (f : perm α) (n : ℕ) : (f^[n]) = ⇑(f ^ n) := (coe_pow _ _).symm
+@[norm_cast] lemma coe_pow (f : perm α) (n : ℕ) : ⇑(f ^ n) = (f^[n]) := rfl
+@[simp] lemma iterate_eq_pow (f : perm α) (n : ℕ) : (f^[n]) = ⇑(f ^ n) := rfl
 
 lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y := f.eq_symm_apply
 
@@ -280,7 +287,7 @@ lemma subtype_perm_inv (f : perm α) (hf) :
 
 private lemma pow_aux (hf : ∀ x, p x ↔ p (f x)) : ∀ {n : ℕ} x, p x ↔ p ((f ^ n) x)
 | 0 x := iff.rfl
-| (n + 1) x := (pow_aux _).trans (hf _)
+| (n + 1) x := (hf _).trans (pow_aux _)
 
 @[simp] lemma subtype_perm_pow (f : perm α) (n : ℕ) (hf) :
   (f.subtype_perm hf : perm {x // p x}) ^ n = (f ^ n).subtype_perm (pow_aux hf) :=

src/group_theory/perm/cycle/basic.lean

@@ -1511,6 +1511,7 @@ begin
   obtain ⟨n, rfl⟩ := hσ.exists_pow_eq (classical.some_spec hσ).1 (mem_support.1 hx),
   apply eq.trans _ (congr rfl (congr rfl (congr rfl
     (congr rfl (hσ.zpowers_equiv_support_symm_apply n).symm)))),
+  simp_rw [←mul_apply, ←pow_succ],
   apply (congr rfl (congr rfl (congr rfl (hσ.zpowers_equiv_support_symm_apply (n + 1))))).trans _,
   simp only [ne.def, is_cycle.zpowers_equiv_support_apply,
     subtype.coe_mk, zpowers_equiv_zpowers_apply],

src/group_theory/perm/cycle/type.lean

@@ -479,7 +479,8 @@ begin
     (λ s, by rw [hf2, add_tsub_cancel_of_le hp.out.one_lt.le, hf3])
     (λ s, by rw [hf2, tsub_add_cancel_of_le hp.out.one_lt.le, hf3]),
   have hσ : ∀ k v, (σ ^ k) v = f k v :=
-  λ k v, nat.rec (hf1 v).symm (λ k hk, eq.trans (by exact congr_arg σ hk) (hf2 k 1 v)) k,
+  λ k v, nat.rec (hf1 v).symm (λ k hk, by { rw pow_succ,
+    exact eq.trans (by exact congr_arg σ hk) (hf2 k 1 v)}) k,
   replace hσ : σ ^ (p ^ 1) = 1 := perm.ext (λ v, by rw [pow_one, hσ, hf3, one_apply]),
   let v₀ : vectors_prod_eq_one G p :=
     ⟨vector.replicate p 1, (list.prod_replicate p 1).trans (one_pow p)⟩,