[Merged by Bors] - chore: Delete Algebra.GroupWithZero.Power

Mathlib.lean

@@ -266,7 +266,6 @@ import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.GroupWithZero.NeZero
 import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.GroupWithZero.Pi
-import Mathlib.Algebra.GroupWithZero.Power
 import Mathlib.Algebra.GroupWithZero.Semiconj
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.GroupWithZero.Units.Equiv

Mathlib/Algebra/Field/Power.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Field.Defs
-import Mathlib.Algebra.GroupWithZero.Power
+import Mathlib.Algebra.GroupWithZero.Commute
 import Mathlib.Algebra.GroupWithZero.Bitwise
 import Mathlib.Algebra.Parity
 

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.GroupWithZero.NeZero
 import Mathlib.Algebra.Group.OrderSynonym
+import Mathlib.Data.Int.Defs
 
 #align_import algebra.group_with_zero.basic from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 
@@ -443,6 +444,56 @@ theorem mul_right_surjective₀ {a : G₀} (h : a ≠ 0) : Surjective fun g => g
   ⟨g * a⁻¹, by simp [mul_assoc, inv_mul_cancel h]⟩
 #align mul_right_surjective₀ mul_right_surjective₀
 
+lemma zero_zpow : ∀ n : ℤ, n ≠ 0 → (0 : G₀) ^ n = 0
+  | (n : ℕ), h => by rw [zpow_natCast, zero_pow]; simpa [Int.natCast_eq_zero] using h
+  | .negSucc n, _ => by simp
+#align zero_zpow zero_zpow
+
+lemma zero_zpow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0 := by
+  split_ifs with h
+  · rw [h, zpow_zero]
+  · rw [zero_zpow _ h]
+#align zero_zpow_eq zero_zpow_eq
+
+lemma zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
+  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
+  | .negSucc 0 => by erw [zpow_zero, zpow_negSucc, pow_one, inv_mul_cancel ha]
+  | .negSucc (n + 1) => by
+    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ,
+      zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel ha,
+      mul_one]
+#align zpow_add_one₀ zpow_add_one₀
+
+lemma zpow_sub_one₀ (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
+  calc
+    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := by rw [mul_assoc, mul_inv_cancel ha, mul_one]
+    _ = a ^ n * a⁻¹ := by rw [← zpow_add_one₀ ha, Int.sub_add_cancel]
+#align zpow_sub_one₀ zpow_sub_one₀
+
+lemma zpow_add₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
+  induction' n using Int.induction_on with n ihn n ihn
+  · simp
+  · simp only [← Int.add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
+  · rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, Int.add_sub_assoc]
+#align zpow_add₀ zpow_add₀
+
+lemma zpow_add' {m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) :
+    a ^ (m + n) = a ^ m * a ^ n := by
+  by_cases hm : m = 0
+  · simp [hm]
+  by_cases hn : n = 0
+  · simp [hn]
+  by_cases ha : a = 0
+  · subst a
+    simp only [false_or_iff, eq_self_iff_true, not_true, Ne, hm, hn, false_and_iff,
+      or_false_iff] at h
+    rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
+  · exact zpow_add₀ ha m n
+#align zpow_add' zpow_add'
+
+lemma zpow_one_add₀ (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i := by rw [zpow_add₀ h, zpow_one]
+#align zpow_one_add₀ zpow_one_add₀
+
 end GroupWithZero
 
 section CommGroupWithZero
@@ -453,6 +504,12 @@ theorem div_mul_eq_mul_div₀ (a b c : G₀) : a / c * b = a * b / c := by
   simp_rw [div_eq_mul_inv, mul_assoc, mul_comm c⁻¹]
 #align div_mul_eq_mul_div₀ div_mul_eq_mul_div₀
 
+lemma div_sq_cancel (a b : G₀) : a ^ 2 * b / a = a * b := by
+  obtain rfl | ha := eq_or_ne a 0
+  · simp
+  · rw [sq, mul_assoc, mul_div_cancel_left₀ _ ha]
+#align div_sq_cancel div_sq_cancel
+
 end CommGroupWithZero
 
 /-! ### Order dual -/

Mathlib/Algebra/GroupWithZero/Bitwise.lean

@@ -3,7 +3,8 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Mathlib.Algebra.GroupWithZero.Power
+import Mathlib.Algebra.GroupPower.Basic
+import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Data.Int.Bitwise
 
 #align_import algebra.group_with_zero.power from "leanprover-community/mathlib"@"46a64b5b4268c594af770c44d9e502afc6a515cb"

Mathlib/Algebra/GroupWithZero/Commute.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Group.Commute.Units
 import Mathlib.Tactic.Nontriviality
 
 #align_import algebra.group_with_zero.commute from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
+#align_import algebra.group_with_zero.power from "leanprover-community/mathlib"@"46a64b5b4268c594af770c44d9e502afc6a515cb"
 
 /-!
 # Lemmas about commuting elements in a `MonoidWithZero` or a `GroupWithZero`.
@@ -89,3 +90,12 @@ theorem div_left (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c :=
 #align commute.div_left Commute.div_left
 
 end Commute
+
+section GroupWithZero
+variable {G₀ : Type*} [GroupWithZero G₀] {a : G₀} {m n : ℕ}
+
+theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
+  (Commute.refl a).inv_left₀.pow_pow m n
+#align pow_inv_comm₀ pow_inv_comm₀
+
+end GroupWithZero

Mathlib/Algebra/GroupWithZero/Semiconj.lean

@@ -64,4 +64,34 @@ theorem div_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
   exact h.mul_right h'.inv_right₀
 #align semiconj_by.div_right SemiconjBy.div_right
 
+lemma zpow_right₀ {a x y : G₀} (h : SemiconjBy a x y) : ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
+  | (n : ℕ) => by simp [h.pow_right n]
+  | .negSucc n => by simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]
+#align semiconj_by.zpow_right₀ SemiconjBy.zpow_right₀
+
 end SemiconjBy
+
+namespace Commute
+variable [GroupWithZero G₀] {a b : G₀}
+
+lemma zpow_right₀ (h : Commute a b) : ∀ m : ℤ, Commute a (b ^ m) := SemiconjBy.zpow_right₀ h
+#align commute.zpow_right₀ Commute.zpow_right₀
+
+lemma zpow_left₀ (h : Commute a b) (m : ℤ) : Commute (a ^ m) b := (h.symm.zpow_right₀ m).symm
+#align commute.zpow_left₀ Commute.zpow_left₀
+
+lemma zpow_zpow₀ (h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n) :=
+  (h.zpow_left₀ m).zpow_right₀ n
+#align commute.zpow_zpow₀ Commute.zpow_zpow₀
+
+lemma zpow_self₀ (a : G₀) (n : ℤ) : Commute (a ^ n) a := (Commute.refl a).zpow_left₀ n
+#align commute.zpow_self₀ Commute.zpow_self₀
+
+lemma self_zpow₀ (a : G₀) (n : ℤ) : Commute a (a ^ n) := (Commute.refl a).zpow_right₀ n
+#align commute.self_zpow₀ Commute.self_zpow₀
+
+lemma zpow_zpow_self₀ (a : G₀) (m n : ℤ) : Commute (a ^ m) (a ^ n) :=
+  (Commute.refl a).zpow_zpow₀ m n
+#align commute.zpow_zpow_self₀ Commute.zpow_zpow_self₀
+
+end Commute