Powers of elements of groups with an adjoined zero element

In this file we define integer power functions for groups with an adjoined zero element. This generalises the integer power function on a division ring.

theorem pow_sub₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) {m : ℕ} {n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹

theorem pow_sub_of_lt {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) {m : ℕ} {n : ℕ} (h : n < m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹

theorem pow_inv_comm₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (m : ℕ) (n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

theorem inv_pow_sub₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {m : ℕ} {n : ℕ} (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

theorem inv_pow_sub_of_lt {G₀ : Type u_1} [GroupWithZero G₀] {m : ℕ} {n : ℕ} (a : G₀) (h : n < m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

theorem zero_zpow {G₀ : Type u_1} [GroupWithZero G₀] (z : ℤ) : z ≠ 0 → 0 ^ z = 0

theorem zero_zpow_eq {G₀ : Type u_1} [GroupWithZero G₀] (n : ℤ) : 0 ^ n = if n = 0 then 1 else 0

theorem zpow_add_one₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) : a ^ (n + 1) = a ^ n * a

theorem zpow_sub_one₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹

theorem zpow_add₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (m : ℤ) (n : ℤ) : a ^ (m + n) = a ^ m * a ^ n

theorem zpow_add' {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {m : ℤ} {n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) : a ^ (m + n) = a ^ m * a ^ n

theorem zpow_one_add₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i

theorem SemiconjBy.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {x : G₀} {y : G₀} (h : SemiconjBy a x y) (m : ℤ) : SemiconjBy a (x ^ m) (y ^ m)

theorem Commute.zpow_right₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ℤ) : Commute a (b ^ m)

theorem Commute.zpow_left₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ℤ) : Commute (a ^ m) b

theorem Commute.zpow_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {b : G₀} (h : Commute a b) (m : ℤ) (n : ℤ) : Commute (a ^ m) (b ^ n)

theorem Commute.zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) : Commute (a ^ n) a

theorem Commute.self_zpow₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (n : ℤ) : Commute a (a ^ n)

theorem Commute.zpow_zpow_self₀ {G₀ : Type u_1} [GroupWithZero G₀] (a : G₀) (m : ℤ) (n : ℤ) : Commute (a ^ m) (a ^ n)

theorem zpow_ne_zero_of_ne_zero {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (z : ℤ) : a ^ z ≠ 0

theorem zpow_sub₀ {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (z1 : ℤ) (z2 : ℤ) : a ^ (z1 - z2) = a ^ z1 / a ^ z2

theorem zpow_eq_zero {G₀ : Type u_1} [GroupWithZero G₀] {x : G₀} {n : ℤ} (h : x ^ n = 0) : x = 0

theorem zpow_eq_zero_iff {G₀ : Type u_1} [GroupWithZero G₀] {a : G₀} {n : ℤ} (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0

theorem zpow_ne_zero {G₀ : Type u_1} [GroupWithZero G₀] {x : G₀} (n : ℤ) : x ≠ 0 → x ^ n ≠ 0

theorem zpow_neg_mul_zpow_self {G₀ : Type u_1} [GroupWithZero G₀] (n : ℤ) {x : G₀} (h : x ≠ 0) : x ^ (-n) * x ^ n = 1

theorem div_sq_cancel {G₀ : Type u_1} [CommGroupWithZero G₀] (a : G₀) (b : G₀) : a ^ 2 * b / a = a * b