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 : ℕ) (a : n ≠ 0) :
0 ^ n = 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 pow_eq_zero' {M : Type u_1} [monoid_with_zero M] [no_zero_divisors M] {a : M} {n : ℕ} (H : a ^ n = 0) :
a = 0

source
theorem pow_ne_zero' {M : Type u_1} [monoid_with_zero M] [no_zero_divisors M] {a : M} (n : ℕ) (h : a ≠ 0) :
a ^ n ≠ 0

source
@[simp]
theorem inv_pow' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℕ) :
a⁻¹ ^ n = (a ^ 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_inv_comm' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (m n : ℕ) :
(a⁻¹ ^ m) * a ^ n = (a ^ n) * a⁻¹ ^ m

source
def fpow {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (a_1 : ℤ) :
G₀

The power operation in a group with zero. This extends monoid.pow to negative integers with the definition a ^ (-n) = (a ^ n)⁻¹.

Equations
source
@[instance]
def int.has_pow {G₀ : Type u_1} [group_with_zero G₀] :
has_pow G₀ ℤ

Equations
source
@[simp]
theorem fpow_coe_nat {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℕ) :
a ^ ↑n = a ^ n

source
theorem fpow_of_nat {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℕ) :
a ^ int.of_nat n = a ^ n

source
@[simp]
theorem fpow_neg_succ_of_nat {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℕ) :
a ^ -[1+ n] = (a ^ n.succ)⁻¹

source
@[simp]
theorem fpow_zero {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) :
a ^ 0 = 1

source
@[simp]
theorem fpow_one {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) :
a ^ 1 = a

source
@[simp]
theorem one_fpow {G₀ : Type u_1} [group_with_zero G₀] (n : ℤ) :
1 ^ n = 1

source
theorem zero_fpow {G₀ : Type u_1} [group_with_zero G₀] (z : ℤ) (a : z ≠ 0) :
0 ^ z = 0

source
@[simp]
theorem fpow_neg {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
a ^ -n = (a ^ n)⁻¹

source
theorem fpow_neg_one {G₀ : Type u_1} [group_with_zero G₀] (x : G₀) :
x ^ -1 = x⁻¹

source
theorem inv_fpow {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
a⁻¹ ^ n = (a ^ n)⁻¹

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

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

source
theorem fpow_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 fpow_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.fpow_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.fpow_right {G₀ : Type u_1} [group_with_zero G₀] {a b : G₀} (h : commute a b) (m : ℤ) :
commute a (b ^ m)

source
theorem commute.fpow_left {G₀ : Type u_1} [group_with_zero G₀] {a b : G₀} (h : commute a b) (m : ℤ) :
commute (a ^ m) b

source
theorem commute.fpow_fpow {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.fpow_self {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
commute (a ^ n) a

source
theorem commute.self_fpow {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :
commute a (a ^ n)

source
theorem commute.fpow_fpow_self {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (m n : ℤ) :
commute (a ^ m) (a ^ n)

source
theorem fpow_mul {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (m n : ℤ) :
a ^ m * n = (a ^ m) ^ n

source
theorem fpow_mul' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (m n : ℤ) :
a ^ m * n = (a ^ n) ^ m

source
@[simp]
theorem units.coe_gpow' {G₀ : Type u_1} [group_with_zero G₀] (u : units G₀) (n : ℤ) :
↑(u ^ n) = ↑u ^ n

source
theorem fpow_ne_zero_of_ne_zero {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (z : ℤ) :
a ^ z ≠ 0

source
theorem fpow_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 commute.mul_fpow {G₀ : Type u_1} [group_with_zero G₀] {a b : G₀} (h : commute a b) (i : ℤ) :
(a * b) ^ i = (a ^ i) * b ^ i

source
theorem mul_fpow {G₀ : Type u_1} [comm_group_with_zero G₀] (a b : G₀) (m : ℤ) :
(a * b) ^ m = (a ^ m) * b ^ m

source
theorem fpow_eq_zero {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} {n : ℤ} (h : x ^ n = 0) :
x = 0

source
theorem fpow_ne_zero {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} (n : ℤ) (a : x ≠ 0) :
x ^ n ≠ 0

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

source
theorem one_div_pow {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (n : ℕ) :
(1 / a) ^ n = 1 / a ^ n

source
theorem one_div_fpow {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (n : ℤ) :
(1 / a) ^ n = 1 / a ^ n

source
@[simp]
theorem div_pow {G₀ : Type u_1} [comm_group_with_zero G₀] (a b : G₀) (n : ℕ) :
(a / b) ^ n = a ^ n / b ^ n

source
@[simp]
theorem div_fpow {G₀ : Type u_1} [comm_group_with_zero G₀] (a : G₀) {b : G₀} (n : ℤ) :
(a / b) ^ n = a ^ n / b ^ n

source
theorem div_sq_cancel {G₀ : Type u_1} [comm_group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (b : G₀) :
(a ^ 2) * b / a = a * b

source
theorem monoid_hom.map_fpow {G₀ : Type u_1} {G₀' : Type u_2} [group_with_zero G₀] [group_with_zero G₀'] (f : G₀ →* G₀') (h0 : ⇑f 0 = 0) (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.