mathlib docs: algebra.group_with_zero

source

@[simp]

theorem zero_pow' {M : Type u_1} [monoid_with_zero M] (n : ℕ) :

n ≠ 0 → 0 ^ 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_eq_zero' {G₀ : Type u_1} [group_with_zero G₀] {g : G₀} {n : ℕ} :

g ^ n = 0 → g = 0

source

theorem pow_ne_zero' {G₀ : Type u_1} [group_with_zero G₀] {g : G₀} (n : ℕ) :

g ≠ 0 → g ^ n ≠ 0

source

theorem pow_sub' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) {m n : ℕ} :

a ≠ 0 → 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₀] :

G₀ → ℤ → G₀

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

Equations

fpow a -[1+ n] = (a ^ n.succ)⁻¹
fpow a (int.of_nat n) = a ^ n

source

@[instance]

def int.has_pow {G₀ : Type u_1} [group_with_zero G₀] :

has_pow G₀ ℤ

Equations

int.has_pow = {pow := fpow _inst_1}

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 : ℤ) :

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 : ℤ} :

x ^ n = 0 → x = 0

source

theorem fpow_ne_zero {G₀ : Type u_1} [group_with_zero G₀] {x : G₀} (n : ℤ) :

x ≠ 0 → x ^ n ≠ 0

source

theorem fpow_neg_mul_fpow_self {G₀ : Type u_1} [group_with_zero G₀] (n : ℤ) {x : G₀} :

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

mathlib documentation

algebra.group_with_zero_power

Powers of elements of groups with an adjoined zero element

General documentation

Additional documentation

Library

mathlib documentation

algebra.​group_with_zero_power

Powers of elements of groups with an adjoined zero element

General documentation

Additional documentation

Library

algebra.group_with_zero_power