feat: mulLeft is a monoid hom (#1348)

Match leanprover-community/mathlib#17900

Mathlib/Algebra/Hom/Iterate.lean

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module algebra.hom.iterate
-! leanprover-community/mathlib commit 550b58538991c8977703fdeb7c9d51a5aa27df11
+! leanprover-community/mathlib commit 792a2a264169d64986541c6f8f7e3bbb6acb6295
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathlib.Logic.Function.Iterate
-import Mathlib.GroupTheory.Perm.Basic
+import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.GroupTheory.GroupAction.Opposite
 
 /-!
@@ -170,10 +169,6 @@ theorem iterate_map_zsmul (n : ℕ) (m : ℤ) (x : R) : (f^[n]) (m • x) = m 
 
 end RingHom
 
-theorem Equiv.Perm.coe_pow {α : Type _} (f : Equiv.Perm α) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
-  hom_coe_pow _ rfl (fun _ _ => rfl) _ _
-#align equiv.perm.coe_pow Equiv.Perm.coe_pow
-
 --what should be the namespace for this section?
 section Monoid
 

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module dynamics.fixed_points.basic
-! leanprover-community/mathlib commit 550b58538991c8977703fdeb7c9d51a5aa27df11
+! leanprover-community/mathlib commit 792a2a264169d64986541c6f8f7e3bbb6acb6295
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -114,7 +114,7 @@ protected theorem perm_inv (h : IsFixedPt e x) : IsFixedPt (⇑e⁻¹) x :=
 #align function.is_fixed_pt.perm_inv Function.IsFixedPt.perm_inv
 
 protected theorem perm_pow (h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x := by
-  rw [← Equiv.Perm.iterate_eq_pow]
+  rw [Equiv.Perm.coe_pow]
   exact h.iterate _
 #align function.is_fixed_pt.perm_pow Function.IsFixedPt.perm_pow
 

Mathlib/GroupTheory/Perm/Basic.lean

@@ -4,14 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 
 ! This file was ported from Lean 3 source module group_theory.perm.basic
-! leanprover-community/mathlib commit d4f69d96f3532729da8ebb763f4bc26fcf640f06
+! leanprover-community/mathlib commit 792a2a264169d64986541c6f8f7e3bbb6acb6295
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Algebra.Group.Pi
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Group.Prod
-import Mathlib.Logic.Function.Iterate
+import Mathlib.Algebra.Hom.Iterate
 
 /-!
 # The group of permutations (self-equivalences) of a type `α`
@@ -93,15 +92,13 @@ theorem inv_def (f : Perm α) : f⁻¹ = f.symm :=
   rfl
 #align equiv.perm.inv_def Equiv.Perm.inv_def
 
-@[simp]
-theorem coe_mul (f g : Perm α) : ⇑(f * g) = f ∘ g :=
-  rfl
-#align equiv.perm.coe_mul Equiv.Perm.coe_mul
-
-@[simp]
-theorem coe_one : ⇑(1 : Perm α) = id :=
-  rfl
+@[simp, norm_cast] lemma coe_one : ⇑(1 : Perm α) = id := rfl
 #align equiv.perm.coe_one Equiv.Perm.coe_one
+@[simp, norm_cast] lemma coe_mul (f g : Perm α) : ⇑(f * g) = f ∘ g := rfl
+#align equiv.perm.coe_mul Equiv.Perm.coe_mul
+@[simp, norm_cast] lemma coe_pow (f : Perm α) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
+hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
+#align equiv.perm.coe_pow Equiv.Perm.coe_pow
 
 theorem eq_inv_iff_eq {f : Perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=
   f.eq_symm_apply
@@ -116,14 +113,6 @@ theorem zpow_apply_comm {α : Type _} (σ : Perm α) (m n : ℤ) {x : α} :
   rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]
 #align equiv.perm.zpow_apply_comm Equiv.Perm.zpow_apply_comm
 
-@[simp]
-theorem iterate_eq_pow (f : Perm α) : ∀ n, f^[n] = ⇑(f ^ n)
-  | 0 => rfl
-  | n + 1 => by
-    -- Porting note: needed to pass `n` to show termination.
-    rw [Function.iterate_succ, pow_succ', iterate_eq_pow f n, coe_mul]
-#align equiv.perm.iterate_eq_pow Equiv.Perm.iterate_eq_pow
-
 /-! 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
@@ -584,4 +573,71 @@ theorem swap_mul_swap_mul_swap {x y z : α} (hwz : x ≠ y) (hxz : x ≠ z) :
 
 end Swap
 
+section AddGroup
+variable [AddGroup α] (a b : α)
+
+@[simp] lemma addLeft_zero : Equiv.addLeft (0 : α) = 1 := ext zero_add
+@[simp] lemma addRight_zero : Equiv.addRight (0 : α) = 1 := ext add_zero
+
+@[simp] lemma addLeft_add : Equiv.addLeft (a + b) = Equiv.addLeft a * Equiv.addLeft b :=
+ext $ add_assoc _ _
+
+@[simp] lemma addRight_add : Equiv.addRight (a + b) = Equiv.addRight b * Equiv.addRight a :=
+ext $ fun _ ↦ (add_assoc _ _ _).symm
+
+@[simp] lemma inv_addLeft : (Equiv.addLeft a)⁻¹ = Equiv.addLeft (-a) := Equiv.coe_inj.1 rfl
+@[simp] lemma inv_addRight : (Equiv.addRight a)⁻¹ = Equiv.addRight (-a) := Equiv.coe_inj.1 rfl
+
+@[simp] lemma pow_addLeft (n : ℕ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a) :=
+by ext; simp [Perm.coe_pow]
+
+@[simp] lemma pow_addRight (n : ℕ) : Equiv.addRight a ^ n = Equiv.addRight (n • a) :=
+by ext; simp [Perm.coe_pow]
+
+@[simp] lemma zpow_addLeft (n : ℤ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a) :=
+(map_zsmul (⟨⟨Equiv.addLeft, addLeft_zero⟩, addLeft_add⟩ : α →+ Additive (Perm α)) _ _).symm
+
+@[simp] lemma zpow_addRight : ∀ (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
+| (Int.ofNat n) => by simp
+| (Int.negSucc n) => by simp
+
+end AddGroup
+
+section Group
+variable [Group α] (a b : α)
+
+@[simp, to_additive] lemma mulLeft_one : Equiv.mulLeft (1 : α) = 1 := ext one_mul
+@[simp, to_additive] lemma mulRight_one : Equiv.mulRight (1 : α) = 1 := ext mul_one
+
+@[simp, to_additive] lemma mulLeft_mul :
+  Equiv.mulLeft (a * b) = Equiv.mulLeft a * Equiv.mulLeft b :=
+ext $ mul_assoc _ _
+
+@[simp, to_additive] lemma mulRight_mul :
+  Equiv.mulRight (a * b) = Equiv.mulRight b * Equiv.mulRight a :=
+ext $ fun _ ↦ (mul_assoc _ _ _).symm
+
+@[simp, to_additive inv_addLeft]
+lemma inv_mulLeft : (Equiv.mulLeft a)⁻¹ = Equiv.mulLeft a⁻¹ := Equiv.coe_inj.1 rfl
+@[simp, to_additive inv_addRight]
+lemma inv_mulRight : (Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹ := Equiv.coe_inj.1 rfl
+
+@[simp, to_additive pow_addLeft]
+lemma pow_mulLeft (n : ℕ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) :=
+by ext; simp [Perm.coe_pow]
+
+@[simp, to_additive pow_addRight]
+lemma pow_mulRight (n : ℕ) : Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n) :=
+by ext; simp [Perm.coe_pow]
+
+@[simp, to_additive zpow_addLeft]
+lemma zpow_mulLeft (n : ℤ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) :=
+(map_zpow (⟨⟨Equiv.mulLeft, mulLeft_one⟩, mulLeft_mul⟩ : α →* Perm α) _ _).symm
+
+@[simp, to_additive zpow_addRight]
+lemma zpow_mulRight : ∀ n : ℤ, Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
+| (Int.ofNat n) => by simp
+| (Int.negSucc n) => by simp
+
+end Group
 end Equiv