mathlib documentation

algebra.group_with_zero.power

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
@[simp]
theorem zero_pow' {M : Type u_1} [monoid_with_zero M] (n : ℕ) :
n ≠ 0 → 0 ^ n = 0
source
theorem ne_zero_pow {M : Type u_1} [monoid_with_zero M] {a : M} {n : ℕ} (hn : n ≠ 0) :
a ^ n ≠ 0 → a ≠ 0
source
@[simp]
theorem zero_pow_eq_zero {M : Type u_1} [monoid_with_zero M] [nontrivial M] {n : ℕ} :
0 ^ n = 0 ↔ 0 < n
source
theorem ring.inverse_pow {M : Type u_1} [monoid_with_zero M] (r : M) (n : ℕ) :
ring.inverse r ^ n = ring.inverse (r ^ n)
source
theorem pow_sub₀ {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem pow_sub_of_lt {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) {m n : ℕ} (h : n < m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem pow_inv_comm₀ {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (m n : ℕ) :
a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
source
theorem inv_pow_sub₀ {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} {m n : ℕ} (ha : a ≠ 0) (h : n ≤ m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
source
theorem inv_pow_sub_of_lt {G₀ : Type u_1} [group_with_zero G₀] {m n : ℕ} (a : G₀) (h : n < m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
source
theorem zero_zpow {G₀ : Type u_1} [group_with_zero G₀] (z : ℤ) :
z ≠ 0 → 0 ^ z = 0
source
theorem zero_zpow_eq {G₀ : Type u_1} [group_with_zero G₀] (n : ℤ) :
0 ^ n = ite (n = 0) 1 0
source
theorem zpow_add_one₀ {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) :
a ^ (n + 1) = a ^ n * a
source
theorem zpow_sub_one₀ {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) :
a ^ (n - 1) = a ^ n * a⁻¹
source
theorem zpow_add₀ {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (m n : ℤ) :
a ^ (m + n) = a ^ m * a ^ n
source
theorem zpow_add' {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} {m n : ℤ} (h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0) :
a ^ (m + n) = a ^ m * a ^ n
source
theorem zpow_one_add₀ {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) (i : ℤ) :
a ^ (1 + i) = a * a ^ i
source
theorem semiconj_by.zpow_right₀ {G₀ : Type u_1} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) (m : ℤ) :
semiconj_by a (x ^ m) (y ^ m)
source
theorem commute.zpow_right₀ {G₀ : Type u_1} [group_with_zero G₀] {a b : G₀} (h : commute a b) (m : ℤ) :
commute a (b ^ m)
source
theorem commute.zpow_left₀ {G₀ : Type u_1} [group_with_zero G₀] {a b : G₀} (h : commute a b) (m : ℤ) :
commute (a ^ m) b
source
theorem commute.zpow_zpow₀ {G₀ : Type u_1} [group_with_zero G₀] {a b : G₀} (h : commute a b) (m n : ℤ) :
commute (a ^ m) (b ^ n)
source
theorem commute.zpow_self₀ {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
commute (a ^ n) a
source
theorem commute.self_zpow₀ {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
commute a (a ^ n)
source
theorem commute.zpow_zpow_self₀ {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (m n : ℤ) :
commute (a ^ m) (a ^ n)
source
theorem zpow_bit1₀ {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
a ^ bit1 n = a ^ n * a ^ n * a
source
@[simp, norm_cast]
theorem units.coe_zpow₀ {G₀ : Type u_1} [group_with_zero G₀] (u : G₀ˣ) (n : ℤ) :
↑(u ^ n) = ↑u ^ n
source
theorem zpow_ne_zero_of_ne_zero {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (z : ℤ) :
a ^ z ≠ 0
source
theorem zpow_sub₀ {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (z1 z2 : ℤ) :
a ^ (z1 - z2) = a ^ z1 / a ^ z2
source
theorem zpow_bit1' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
a ^ bit1 n = (a * a) ^ n * a
source
theorem zpow_eq_zero {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} {n : ℤ} (h : x ^ n = 0) :
x = 0
source
theorem zpow_eq_zero_iff {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} {n : ℤ} (hn : 0 < n) :
a ^ n = 0 ↔ a = 0
source
theorem zpow_ne_zero {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} (n : ℤ) :
x ≠ 0 → x ^ n ≠ 0
source
theorem zpow_neg_mul_zpow_self {G₀ : Type u_1} [group_with_zero G₀] (n : ℤ) {x : G₀} (h : x ≠ 0) :
x ^ -n * x ^ n = 1
source
theorem div_sq_cancel {G₀ : Type u_1} [comm_group_with_zero G₀] (a b : G₀) :
a ^ 2 * b / a = a * b
source
theorem monoid_with_zero_hom.map_zpow {G₀ : Type u_1} {G₀' : Type u_2} [group_with_zero G₀] [group_with_zero G₀'] (f : G₀ →*₀ G₀') (x : G₀) (n : ℤ) :
⇑f (x ^ n) = ⇑f x ^ n

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

source
theorem pow_minus_two_nonneg {R : Type u_1} [linear_ordered_field R] {a : R} :
0 ≤ a ^ -2