# 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} [] (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} [] (a : G₀) {m : } {n : } (h : n < m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
theorem pow_inv_comm₀ {G₀ : Type u_1} [] (a : G₀) (m : ) (n : ) :
a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
theorem inv_pow_sub₀ {G₀ : Type u_1} [] {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} [] {m : } {n : } (a : G₀) (h : n < m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
theorem zero_zpow {G₀ : Type u_1} [] (z : ) :
z 00 ^ z = 0
theorem zero_zpow_eq {G₀ : Type u_1} [] (n : ) :
0 ^ n = if n = 0 then 1 else 0
theorem zpow_add_one₀ {G₀ : Type u_1} [] {a : G₀} (ha : a 0) (n : ) :
a ^ (n + 1) = a ^ n * a
theorem zpow_sub_one₀ {G₀ : Type u_1} [] {a : G₀} (ha : a 0) (n : ) :
a ^ (n - 1) = a ^ n * a⁻¹
theorem zpow_add₀ {G₀ : Type u_1} [] {a : G₀} (ha : a 0) (m : ) (n : ) :
a ^ (m + n) = a ^ m * a ^ n
theorem zpow_add' {G₀ : Type u_1} [] {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} [] {a : G₀} (h : a 0) (i : ) :
a ^ (1 + i) = a * a ^ i
theorem SemiconjBy.zpow_right₀ {G₀ : Type u_1} [] {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} [] {a : G₀} {b : G₀} (h : Commute a b) (m : ) :
Commute a (b ^ m)
theorem Commute.zpow_left₀ {G₀ : Type u_1} [] {a : G₀} {b : G₀} (h : Commute a b) (m : ) :
Commute (a ^ m) b
theorem Commute.zpow_zpow₀ {G₀ : Type u_1} [] {a : G₀} {b : G₀} (h : Commute a b) (m : ) (n : ) :
Commute (a ^ m) (b ^ n)
theorem Commute.zpow_self₀ {G₀ : Type u_1} [] (a : G₀) (n : ) :
Commute (a ^ n) a
theorem Commute.self_zpow₀ {G₀ : Type u_1} [] (a : G₀) (n : ) :
Commute a (a ^ n)
theorem Commute.zpow_zpow_self₀ {G₀ : Type u_1} [] (a : G₀) (m : ) (n : ) :
Commute (a ^ m) (a ^ n)
theorem zpow_ne_zero_of_ne_zero {G₀ : Type u_1} [] {a : G₀} (ha : a 0) (z : ) :
a ^ z 0
theorem zpow_sub₀ {G₀ : Type u_1} [] {a : G₀} (ha : a 0) (z1 : ) (z2 : ) :
a ^ (z1 - z2) = a ^ z1 / a ^ z2
theorem zpow_eq_zero {G₀ : Type u_1} [] {x : G₀} {n : } (h : x ^ n = 0) :
x = 0
theorem zpow_eq_zero_iff {G₀ : Type u_1} [] {a : G₀} {n : } (hn : n 0) :
a ^ n = 0 a = 0
theorem zpow_ne_zero {G₀ : Type u_1} [] {x : G₀} (n : ) :
x 0x ^ n 0
theorem zpow_neg_mul_zpow_self {G₀ : Type u_1} [] (n : ) {x : G₀} (h : x 0) :
x ^ (-n) * x ^ n = 1
theorem div_sq_cancel {G₀ : Type u_1} [] (a : G₀) (b : G₀) :
a ^ 2 * b / a = a * b