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.

@[simp]

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

n ≠ 0 → 0 ^ n = 0

theorem ne_zero_pow {M : Type u_1} [monoid_with_zero M] {a : M} {n : ℕ} (hn : n ≠ 0) :

a ^ n ≠ 0 → a ≠ 0

@[simp]

theorem zero_pow_eq_zero {M : Type u_1} [monoid_with_zero M] [nontrivial M] {n : ℕ} :

0 ^ n = 0 ↔ 0 < n

@[simp]

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

a⁻¹ ^ n = (a ^ n)⁻¹

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)⁻¹

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

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

def fpow {G₀ : Type u_1} [group_with_zero G₀] (a : 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

@[instance]

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

has_pow G₀ ℤ

Equations

int.has_pow = {pow := fpow _inst_1}

@[simp]

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

a ^ ↑n = a ^ n

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

a ^ int.of_nat n = a ^ n

@[simp]

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

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

@[simp]

theorem fpow_zero {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) :

a ^ 0 = 1

@[simp]

theorem fpow_one {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) :

a ^ 1 = a

@[simp]

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

1 ^ n = 1

theorem zero_fpow {G₀ : Type u_1} [group_with_zero G₀] (z : ℤ) :

z ≠ 0 → 0 ^ z = 0

@[simp]

theorem fpow_neg {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :

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

theorem fpow_neg_one {G₀ : Type u_1} [group_with_zero G₀] (x : G₀) :

x ^ -1 = x⁻¹

theorem inv_fpow {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :

a⁻¹ ^ n = (a ^ n)⁻¹

theorem fpow_add_one {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) :

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

theorem fpow_sub_one {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (ha : a ≠ 0) (n : ℤ) :

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

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

theorem fpow_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

theorem fpow_one_add {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (h : a ≠ 0) (i : ℤ) :

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

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)

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

commute a (b ^ m)

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

commute (a ^ m) b

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)

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

commute (a ^ n) a

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

commute a (a ^ n)

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

commute (a ^ m) (a ^ n)

theorem fpow_bit0 {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :

a ^ bit0 n = (a ^ n) * a ^ n

theorem fpow_bit1 {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :

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

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

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

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

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

@[simp]

theorem units.coe_gpow' {G₀ : Type u_1} [group_with_zero G₀] (u : units G₀) (n : ℤ) :

↑(u ^ n) = ↑u ^ n

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

a ^ z ≠ 0

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

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

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

(a * b) ^ m = (a ^ m) * b ^ m

theorem fpow_bit0' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :

a ^ bit0 n = (a * a) ^ n

theorem fpow_bit1' {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ℤ) :

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

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

x = 0

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

x ≠ 0 → x ^ n ≠ 0

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

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

(1 / a) ^ n = 1 / a ^ n

theorem one_div_fpow {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (n : ℤ) :

(1 / a) ^ n = 1 / a ^ n

@[simp]

theorem inv_fpow' {G₀ : Type u_1} [group_with_zero G₀] {a : G₀} (n : ℤ) :

a⁻¹ ^ n = a ^ -n

@[simp]

theorem div_pow {G₀ : Type u_1} [comm_group_with_zero G₀] (a b : G₀) (n : ℕ) :

(a / b) ^ n = a ^ n / b ^ n

@[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

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

theorem monoid_with_zero_hom.map_fpow {G₀ : Type u_1} {G₀' : Type u_2} [group_with_zero G₀] [group_with_zero G₀'] (f : monoid_with_zero_hom 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.