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

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

0 ^ n = ite (n = 0) 1 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.