mathlibdocumentation

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} (n : ) :
n 00 ^ n = 0

@[simp]
theorem zero_pow_eq_zero {M : Type u_1} [nontrivial M] {n : } :
0 ^ n = 0 0 < n

theorem pow_eq_zero' {M : Type u_1} {a : M} {n : } :
a ^ n = 0a = 0

theorem pow_ne_zero' {M : Type u_1} {a : M} (n : ) :
a 0a ^ n 0

@[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 : } :
a 0n ma ^ (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₀] :
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
@[instance]
def int.has_pow {G₀ : Type u_1} [group_with_zero G₀] :

Equations
@[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 ^ = a ^ n

@[simp]
theorem fpow_neg_succ_of_nat {G₀ : Type u_1} [group_with_zero G₀] (a : G₀) (n : ) :
a ^ = (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 00 ^ 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 : } :
a 0 m + n 0 m = 0 n = 0a ^ (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 : x y) (m : ) :
(x ^ m) (y ^ m)

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

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

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

theorem mul_fpow {G₀ : Type u_1} (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 : } :
x ^ n = 0x = 0

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

theorem fpow_neg_mul_fpow_self {G₀ : Type u_1} [group_with_zero G₀] (n : ) {x : G₀} :
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 div_pow {G₀ : Type u_1} (a b : G₀) (n : ) :
(a / b) ^ n = a ^ n / b ^ n

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

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

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.