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.

source

ink

theorem pow_sub₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) {m : ℕ} {n : ℕ} (ha : a ≠ 0) (h : n ≤ m) :

a ^ (m - n) = a ^ m * (a ^ n)⁻¹

source

ink

theorem pow_sub_of_lt {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) {m : ℕ} {n : ℕ} (h : n < m) :

a ^ (m - n) = a ^ m * (a ^ n)⁻¹

source

ink

theorem pow_inv_comm₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (m : ℕ) (n : ℕ) :

a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

source

ink

theorem inv_pow_sub₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} {m : ℕ} {n : ℕ} (ha : a ≠ 0) (h : n ≤ m) :

a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

source

ink

theorem inv_pow_sub_of_lt {G₀ : Type u_1} [inst : GroupWithZero G₀] {m : ℕ} {n : ℕ} (a : G₀) (h : n < m) :

a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

source

ink

theorem zero_zpow {G₀ : Type u_1} [inst : GroupWithZero G₀] (z : ℤ) :

z ≠ 0 → 0 ^ z = 0

source

ink

theorem zero_zpow_eq {G₀ : Type u_1} [inst : GroupWithZero G₀] (n : ℤ) :

0 ^ n = if n = 0 then 1 else 0

source

ink

theorem zpow_add_one₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) :

a ^ (n + 1) = a ^ n * a

source

ink

theorem zpow_sub_one₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) :

a ^ (n - 1) = a ^ n * a⁻¹

source

ink

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

a ^ (m + n) = a ^ m * a ^ n

source

ink

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

a ^ (m + n) = a ^ m * a ^ n

source

ink

theorem zpow_one_add₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0) (i : ℤ) :

a ^ (1 + i) = a * a ^ i

source

ink

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

SemiconjBy a (x ^ m) (y ^ m)

source

ink

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

Commute a (b ^ m)

source

ink

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

Commute (a ^ m) b

source

ink

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

Commute (a ^ m) (b ^ n)

source

ink

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

Commute (a ^ n) a

source

ink

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

Commute a (a ^ n)

source

ink

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

Commute (a ^ m) (a ^ n)

source

ink

theorem zpow_bit1₀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (n : ℤ) :

a ^ bit1 n = a ^ n * a ^ n * a

source

ink

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

a ^ z ≠ 0

source

ink

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

a ^ (z1 - z2) = a ^ z1 / a ^ z2

source

ink

theorem zpow_bit1' {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀) (n : ℤ) :

a ^ bit1 n = (a * a) ^ n * a

source

ink

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

x = 0

source

ink

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

a ^ n = 0 ↔ a = 0

source

ink

theorem zpow_ne_zero {G₀ : Type u_1} [inst : GroupWithZero G₀] {x : G₀} (n : ℤ) :

x ≠ 0 → x ^ n ≠ 0

source

ink

theorem zpow_neg_mul_zpow_self {G₀ : Type u_1} [inst : GroupWithZero G₀] (n : ℤ) {x : G₀} (h : x ≠ 0) :

x ^ (-n) * x ^ n = 1

source

ink

theorem div_sq_cancel {G₀ : Type u_1} [inst : CommGroupWithZero G₀] (a : G₀) (b : G₀) :

a ^ 2 * b / a = a * b

source

ink

@[simp]

theorem map_zpow₀ {F : Type u_1} {G₀ : Type u_2} {G₀' : Type u_3} [inst : GroupWithZero G₀] [inst : GroupWithZero G₀'] [inst : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) :

↑f (x ^ n) = ↑f x ^ n

If a monoid homomorphism f between two GroupWithZeros maps 0 to 0, then it maps x^n, n : ℤ, to (f x)^n.