chore: Move zpow lemmas (#9720)

These lemmas can be proved much earlier with little to no change to their proofs.

Part of #9411

Archive/Imo/Imo1998Q2.lean

@@ -3,10 +3,10 @@ Copyright (c) 2020 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.Algebra.BigOperators.Order
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Int.Parity
-import Mathlib.Algebra.BigOperators.Order
-import Mathlib.Tactic.Ring
+import Mathlib.GroupTheory.GroupAction.Ring
 import Mathlib.Tactic.NoncommRing
 
 #align_import imo.imo1998_q2 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"

Archive/MiuLanguage/DecisionSuf.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gihan Marasingha
 -/
 import Archive.MiuLanguage.DecisionNec
+import Mathlib.Data.Nat.Pow
 import Mathlib.Tactic.Linarith
 
 #align_import miu_language.decision_suf from "leanprover-community/mathlib"@"f694c7dead66f5d4c80f446c796a5aad14707f0e"

Mathlib/Algebra/BigOperators/Basic.lean

@@ -5,16 +5,12 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas
 import Mathlib.Algebra.Function.Indicator
-import Mathlib.Algebra.Group.Equiv.Basic
-import Mathlib.Algebra.Group.Pi
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Data.Finset.Powerset
 import Mathlib.Data.Finset.Sigma
 import Mathlib.Data.Finset.Sum
 import Mathlib.Data.Fintype.Pi
-import Mathlib.Data.Multiset.Powerset
-import Mathlib.Data.Set.Pairwise.Basic
+import Mathlib.Data.Int.Cast.Lemmas
 
 #align_import algebra.big_operators.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 

Mathlib/Algebra/CharZero/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Function.Support
-import Mathlib.Algebra.GroupPower.Lemmas
+import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Data.Nat.Cast.Field
 
 #align_import algebra.char_zero.lemmas from "leanprover-community/mathlib"@"acee671f47b8e7972a1eb6f4eed74b4b3abce829"

Mathlib/Algebra/GCDMonoid/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
 import Mathlib.Algebra.Associated
-import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Ring.Regular
 import Mathlib.Tactic.Common
 

Mathlib/Algebra/Group/Conj.lean

@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Chris Hughes, Michael Howes
 -/
 import Mathlib.Algebra.Group.Aut
-import Mathlib.Algebra.Group.Hom.Defs
-import Mathlib.Algebra.Group.Semiconj.Defs
-import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Algebra.Group.Semiconj.Units
 
 #align_import algebra.group.conj from "leanprover-community/mathlib"@"0743cc5d9d86bcd1bba10f480e948a257d65056f"
 

Mathlib/Algebra/GroupPower/Basic.lean

@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import Mathlib.Algebra.Group.Commute.Basic
 import Mathlib.Algebra.GroupWithZero.Defs
+import Mathlib.Data.Int.Defs
 import Mathlib.Tactic.Common
 
 #align_import algebra.group_power.basic from "leanprover-community/mathlib"@"9b2660e1b25419042c8da10bf411aa3c67f14383"
@@ -17,7 +18,7 @@ We separate this from group, because it depends on `ℕ`,
 which in turn depends on other parts of algebra.
 
 This module contains lemmas about `a ^ n` and `n • a`, where `n : ℕ` or `n : ℤ`.
-Further lemmas can be found in `Algebra.GroupPower.Lemmas`.
+Further lemmas can be found in `Algebra.GroupPower.Ring`.
 
 The analogous results for groups with zero can be found in `Algebra.GroupWithZero.Power`.
 
@@ -31,6 +32,8 @@ The analogous results for groups with zero can be found in `Algebra.GroupWithZer
 We adopt the convention that `0^0 = 1`.
 -/
 
+open Int
+
 universe u v w x y z u₁ u₂
 
 variable {α : Type*} {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z}
@@ -333,6 +336,44 @@ protected theorem Commute.mul_zpow (h : Commute a b) : ∀ i : ℤ, (a * b) ^ i
 #align commute.mul_zpow Commute.mul_zpow
 #align add_commute.zsmul_add AddCommute.zsmul_add
 
+-- Note that `mul_zsmul` and `zpow_mul` have the primes swapped
+-- when additivised since their argument order,
+-- and therefore the more "natural" choice of lemma, is reversed.
+@[to_additive mul_zsmul'] lemma zpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
+  | (m : ℕ), (n : ℕ) => by
+    rw [zpow_ofNat, zpow_ofNat, ← pow_mul, ← zpow_ofNat]
+    rfl
+  | (m : ℕ), -[n+1] => by
+    rw [zpow_ofNat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg, inv_inj, ← zpow_ofNat]
+  | -[m+1], (n : ℕ) => by
+    rw [zpow_ofNat, zpow_negSucc, ← inv_pow, ← pow_mul, negSucc_mul_ofNat, zpow_neg, inv_pow,
+      inv_inj, ← zpow_ofNat]
+  | -[m+1], -[n+1] => by
+    rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
+      zpow_ofNat]
+    rfl
+#align zpow_mul zpow_mul
+#align mul_zsmul' mul_zsmul'
+
+@[to_additive mul_zsmul]
+lemma zpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m := by rw [Int.mul_comm, zpow_mul]
+#align zpow_mul' zpow_mul'
+#align mul_zsmul mul_zsmul
+
+set_option linter.deprecated false
+
+@[to_additive bit0_zsmul]
+lemma zpow_bit0 (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := by
+  rw [bit0, ← Int.two_mul, zpow_mul', ← pow_two, ← zpow_coe_nat]; norm_cast
+#align zpow_bit0 zpow_bit0
+#align bit0_zsmul bit0_zsmul
+
+@[to_additive bit0_zsmul']
+theorem zpow_bit0' (a : α) (n : ℤ) : a ^ bit0 n = (a * a) ^ n :=
+  (zpow_bit0 a n).trans ((Commute.refl a).mul_zpow n).symm
+#align zpow_bit0' zpow_bit0'
+#align bit0_zsmul' bit0_zsmul'
+
 end DivisionMonoid
 
 section DivisionCommMonoid
@@ -381,6 +422,106 @@ theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^
 #align inv_pow_sub inv_pow_sub
 #align sub_nsmul_neg sub_nsmul_neg
 
+@[to_additive add_one_zsmul]
+lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
+  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_ofNat, pow_succ']
+  | -[0+1] => by erw [zpow_zero, zpow_negSucc, pow_one, mul_left_inv]
+  | -[n + 1+1] => by
+    rw [zpow_negSucc, pow_succ, mul_inv_rev, inv_mul_cancel_right]
+    rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]
+    exact zpow_negSucc _ _
+#align zpow_add_one zpow_add_one
+#align add_one_zsmul add_one_zsmul
+
+@[to_additive sub_one_zsmul]
+lemma zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
+  calc
+    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := (mul_inv_cancel_right _ _).symm
+    _ = a ^ n * a⁻¹ := by rw [← zpow_add_one, Int.sub_add_cancel]
+#align zpow_sub_one zpow_sub_one
+#align sub_one_zsmul sub_one_zsmul
+
+@[to_additive add_zsmul]
+lemma zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
+  induction n using Int.induction_on with
+  | hz => simp
+  | hp n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
+  | hn n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
+#align zpow_add zpow_add
+#align add_zsmul add_zsmul
+
+@[to_additive one_add_zsmul]
+lemma zpow_one_add (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n := by rw [zpow_add, zpow_one]
+#align zpow_one_add zpow_one_add
+#align one_add_zsmul one_add_zsmul
+
+@[to_additive add_zsmul_self]
+lemma mul_self_zpow (a : G) (n : ℤ) : a * a ^ n = a ^ (n + 1) := by
+  rw [Int.add_comm, zpow_add, zpow_one]
+#align mul_self_zpow mul_self_zpow
+#align add_zsmul_self add_zsmul_self
+
+@[to_additive add_self_zsmul]
+lemma mul_zpow_self (a : G) (n : ℤ) : a ^ n * a = a ^ (n + 1) := (zpow_add_one ..).symm
+#align mul_zpow_self mul_zpow_self
+#align add_self_zsmul add_self_zsmul
+
+@[to_additive sub_zsmul] lemma zpow_sub (a : G) (m n : ℤ) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := by
+  rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]
+#align zpow_sub zpow_sub
+#align sub_zsmul sub_zsmul
+
+@[to_additive] lemma zpow_mul_comm (a : G) (m n : ℤ) : a ^ m * a ^ n = a ^ n * a ^ m := by
+  rw [← zpow_add, Int.add_comm, zpow_add]
+#align zpow_mul_comm zpow_mul_comm
+#align zsmul_add_comm zsmul_add_comm
+
+section bit1
+
+set_option linter.deprecated false
+
+@[to_additive bit1_zsmul]
+lemma zpow_bit1 (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a := by
+  rw [bit1, zpow_add, zpow_bit0, zpow_one]
+#align zpow_bit1 zpow_bit1
+#align bit1_zsmul bit1_zsmul
+
+end bit1
+
+/-- 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`. -/
+@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
+addition by `g` and `-g` on the left. For additive subgroups generated by more than one element, see
+`AddSubgroup.closure_induction_left`."]
+lemma zpow_induction_left {g : G} {P : G → Prop} (h_one : P (1 : G))
+    (h_mul : ∀ a, P a → P (g * a)) (h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n) := by
+  induction' n using Int.induction_on with n ih n ih
+  · rwa [zpow_zero]
+  · rw [Int.add_comm, zpow_add, zpow_one]
+    exact h_mul _ ih
+  · rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
+    exact h_inv _ ih
+#align zpow_induction_left zpow_induction_left
+#align zsmul_induction_left zsmul_induction_left
+
+/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
+by `g` and `g⁻¹` on the right. For subgroups generated by more than one element, see
+`Subgroup.closure_induction_right`. -/
+@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
+addition by `g` and `-g` on the right. For additive subgroups generated by more than one element,
+see `AddSubgroup.closure_induction_right`."]
+lemma zpow_induction_right {g : G} {P : G → Prop} (h_one : P (1 : G))
+    (h_mul : ∀ a, P a → P (a * g)) (h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n) := by
+  induction' n using Int.induction_on with n ih n ih
+  · rwa [zpow_zero]
+  · rw [zpow_add_one]
+    exact h_mul _ ih
+  · rw [zpow_sub_one]
+    exact h_inv _ ih
+#align zpow_induction_right zpow_induction_right
+#align zsmul_induction_right zsmul_induction_right
+
 end Group
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -3,7 +3,9 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.GroupPower.Lemmas
+import Mathlib.Algebra.Ring.Hom.Defs
+import Mathlib.Data.Int.Basic
+import Mathlib.Data.Nat.Basic
 import Mathlib.GroupTheory.GroupAction.Opposite
 
 #align_import algebra.hom.iterate from "leanprover-community/mathlib"@"792a2a264169d64986541c6f8f7e3bbb6acb6295"