chore(Algebra/GroupPower/IterateHom): move all lemmas earlier (#22132)

All lemmas in this file belong earlier. This finally gets rid of the `Algebra.GroupPower` folder, notorious for having caused imports increases in the algebra library (see #11855 for full motivation).

Author: YaelDillies

Mathlib.lean

@@ -397,7 +397,6 @@ import Mathlib.Algebra.Group.Units.Hom
 import Mathlib.Algebra.Group.Units.Opposite
 import Mathlib.Algebra.Group.WithOne.Basic
 import Mathlib.Algebra.Group.WithOne.Defs
-import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.Algebra.GroupWithZero.Action.ConjAct
 import Mathlib.Algebra.GroupWithZero.Action.Defs

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -5,11 +5,9 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.End
 import Mathlib.Algebra.Group.Action.Pi
-import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Algebra.Module.NatInt
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Order.Group.Instances
-import Mathlib.Logic.Function.Iterate
 
 /-!
 # Maps (semi)conjugating a shift to a shift

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -3,9 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import Mathlib.Algebra.Algebra.Defs
 import Mathlib.Algebra.Algebra.NonUnitalHom
-import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 /-!

Mathlib/Algebra/CharP/Lemmas.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Joey van Langen, Casper Putz
 -/
 import Mathlib.Algebra.CharP.Defs
-import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.Data.Nat.Multiplicity
 import Mathlib.Data.Nat.Choose.Sum
 

Mathlib/Algebra/Group/Action/Defs.lean

@@ -338,7 +338,7 @@ lemma Commute.smul_left [Mul α] [SMulCommClass M α α] [IsScalarTower M α α]
 end
 
 section
-variable [Monoid M] [MulAction M α]
+variable [Monoid M] [MulAction M α] {a : M}
 
 @[to_additive]
 lemma smul_smul (a₁ a₂ : M) (b : α) : a₁ • a₂ • b = (a₁ * a₂) • b := (mul_smul _ _ _).symm
@@ -359,6 +359,15 @@ lemma comp_smul_left (a₁ a₂ : M) : (a₁ • ·) ∘ (a₂ • ·) = (((a₁
 
 variable {M}
 
+@[to_additive (attr := simp)]
+theorem smul_iterate (a : M) : ∀ n : ℕ, (a • · : α → α)^[n] = (a ^ n • ·)
+  | 0 => by simp [funext_iff]
+  | n + 1 => by ext; simp [smul_iterate, pow_succ, smul_smul]
+
+@[to_additive]
+lemma smul_iterate_apply (a : M) (n : ℕ) (x : α) : (a • ·)^[n] x = a ^ n • x := by
+  rw [smul_iterate]
+
 /-- Pullback a multiplicative action along an injective map respecting `•`.
 See note [reducible non-instances]. -/
 @[to_additive

Mathlib/Algebra/Group/Basic.lean

@@ -7,7 +7,7 @@ import Aesop
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Nat.Init
 import Mathlib.Data.Int.Init
-import Mathlib.Logic.Function.Basic
+import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.SplitIfs
 
@@ -206,6 +206,27 @@ lemma pow_eq_pow_mod (m : ℕ) (ha : a ^ n = 1) : a ^ m = a ^ (m % n) := by
       _ = a ^ n * (a * b) * b ^ n := by simp only [mul_assoc]
       _ = 1 := by simp [h, pow_mul_pow_eq_one]
 
+@[to_additive (attr := simp)]
+lemma mul_left_iterate (a : M) : ∀ n : ℕ, (a * ·)^[n] = (a ^ n * ·)
+  | 0 =>  by ext; simp
+  | n + 1 => by ext; simp [pow_succ, mul_left_iterate]
+
+@[to_additive (attr := simp)]
+lemma mul_right_iterate (a : M) : ∀ n : ℕ, (· * a)^[n] = (· * a ^ n)
+  | 0 =>  by ext; simp
+  | n + 1 => by ext; simp [pow_succ', mul_right_iterate]
+
+@[to_additive]
+lemma mul_left_iterate_apply_one (a : M) : (a * ·)^[n] 1 = a ^ n := by simp [mul_right_iterate]
+
+@[to_additive]
+lemma mul_right_iterate_apply_one (a : M) : (· * a)^[n] 1 = a ^ n := by simp [mul_right_iterate]
+
+@[to_additive (attr := simp)]
+lemma pow_iterate (k : ℕ) : ∀ n : ℕ, (fun x : M ↦ x ^ k)^[n] = (· ^ k ^ n)
+  | 0 => by ext; simp
+  | n + 1 => by ext; simp [pow_iterate, Nat.pow_succ', pow_mul]
+
 end Monoid
 
 section CommMonoid
@@ -866,6 +887,11 @@ theorem zpow_eq_zpow_emod {x : G} (m : ℤ) {n : ℤ} (h : x ^ n = 1) :
 theorem zpow_eq_zpow_emod' {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) :
     x ^ m = x ^ (m % (n : ℤ)) := zpow_eq_zpow_emod m (by simpa)
 
+@[to_additive (attr := simp)]
+lemma zpow_iterate (k : ℤ) : ∀ n : ℕ, (fun x : G ↦ x ^ k)^[n] = (· ^ k ^ n)
+  | 0 => by ext; simp [Int.pow_zero]
+  | n + 1 => by ext; simp [zpow_iterate, Int.pow_succ', zpow_mul]
+
 /-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
 by `g` and `g⁻¹` on the left. For subgroups generated by more than one element, see
 `Subgroup.closure_induction_left`. -/
@@ -1034,3 +1060,12 @@ theorem multiplicative_of_isTotal (p : α → Prop) (hswap : ∀ {a b}, p a →
   exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
 
 end multiplicative
+
+/-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`. -/
+@[to_additive]
+lemma hom_coe_pow {F : Type*} [Monoid F] (c : F → M → M) (h1 : c 1 = id)
+    (hmul : ∀ f g, c (f * g) = c f ∘ c g) (f : F) : ∀ n, c (f ^ n) = (c f)^[n]
+  | 0 => by
+    rw [pow_zero, h1]
+    rfl
+  | n + 1 => by rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]

Mathlib/Algebra/Group/Commute/Basic.lean

@@ -15,6 +15,29 @@ assert_not_exists MonoidWithZero DenselyOrdered
 
 variable {G : Type*}
 
+section Semigroup
+variable [Semigroup G] {a b c : G}
+
+open Function
+
+@[to_additive]
+lemma SemiconjBy.function_semiconj_mul_left (h : SemiconjBy a b c) :
+    Semiconj (a * ·) (b * ·) (c * ·) := fun j ↦ by simp only [← mul_assoc, h.eq]
+
+@[to_additive]
+lemma Commute.function_commute_mul_left (h : Commute a b) : Function.Commute (a * ·) (b * ·) :=
+  SemiconjBy.function_semiconj_mul_left h
+
+@[to_additive]
+lemma SemiconjBy.function_semiconj_mul_right_swap (h : SemiconjBy a b c) :
+    Function.Semiconj (· * a) (· * c) (· * b) := fun j ↦ by simp only [mul_assoc, ← h.eq]
+
+@[to_additive]
+lemma Commute.function_commute_mul_right (h : Commute a b) : Function.Commute (· * a) (· * b) :=
+  SemiconjBy.function_semiconj_mul_right_swap h
+
+end Semigroup
+
 namespace Commute
 
 section DivisionMonoid

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -57,6 +57,7 @@ MonoidHom, AddMonoidHom
 
 -/
 
+open Function
 
 variable {ι α β M N P : Type*}
 
@@ -1024,3 +1025,39 @@ protected theorem map_mul_inv [Group α] [DivisionMonoid β] (f : α →* β) (g
     f (g * h⁻¹) = f g * (f h)⁻¹ := by simp
 
 end MonoidHom
+
+@[to_additive (attr := simp)]
+lemma iterate_map_mul {M F : Type*} [Mul M] [FunLike F M M] [MulHomClass F M M]
+    (f : F) (n : ℕ) (x y : M) :
+    f^[n] (x * y) = f^[n] x * f^[n] y :=
+  Function.Semiconj₂.iterate (map_mul f) n x y
+
+@[to_additive (attr := simp)]
+lemma iterate_map_one {M F : Type*} [One M] [FunLike F M M] [OneHomClass F M M]
+    (f : F) (n : ℕ) :
+    f^[n] 1 = 1 :=
+  iterate_fixed (map_one f) n
+
+@[to_additive (attr := simp)]
+lemma iterate_map_inv {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M]
+    (f : F) (n : ℕ) (x : M) :
+    f^[n] x⁻¹ = (f^[n] x)⁻¹ :=
+  Commute.iterate_left (map_inv f) n x
+
+@[to_additive (attr := simp)]
+lemma iterate_map_div {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M]
+    (f : F) (n : ℕ) (x y : M) :
+    f^[n] (x / y) = f^[n] x / f^[n] y :=
+  Semiconj₂.iterate (map_div f) n x y
+
+@[to_additive (attr := simp)]
+lemma iterate_map_pow {M F : Type*} [Monoid M] [FunLike F M M] [MonoidHomClass F M M]
+    (f : F) (n : ℕ) (x : M) (k : ℕ) :
+    f^[n] (x ^ k) = f^[n] x ^ k :=
+  Commute.iterate_left (map_pow f · k) n x
+
+@[to_additive (attr := simp)]
+lemma iterate_map_zpow {M F : Type*} [Group M] [FunLike F M M] [MonoidHomClass F M M]
+    (f : F) (n : ℕ) (x : M) (k : ℤ) :
+    f^[n] (x ^ k) = f^[n] x ^ k :=
+  Commute.iterate_left (map_zpow f · k) n x

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne Baanen,
   Frédéric Dupuis, Heather Macbeth
 -/
-import Mathlib.Algebra.GroupPower.IterateHom
-import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Algebra.Module.Equiv.Opposite
 import Mathlib.Algebra.NoZeroSMulDivisors.Defs