mathlib documentation

algebra.group_power.basic

Power operations on monoids and groups

The power operation on monoids and groups. We separate this from group, because it depends on , which in turn depends on other parts of algebra.

This module contains the definitions of monoid.pow and group.pow and their additive counterparts nsmul and gsmul, along with a few lemmas. Further lemmas can be found in algebra.group_power.lemmas.

Notation

The class has_pow α β provides the notation a^b for powers. We define instances of has_pow M ℕ, for monoids M, and has_pow G ℤ for groups G.

We also define infix operators •ℕ and •ℤ for scalar multiplication by a natural and an integer numbers, respectively.

Implementation details

We adopt the convention that 0^0 = 1.

This module provides the instance has_pow ℕ ℕ (via monoid.has_pow) and is imported by data.nat.basic, so it has to live low in the import hierarchy. Not all of its imports are needed yet; the intent is to move more lemmas here from .lemmas so that they are available in data.nat.basic, and the imports will be required then.

def monoid.pow {M : Type u} [has_mul M] [has_one M] :
M → → M

The power operation in a monoid. a^n = a*a*...*a n times.

Equations
def nsmul {A : Type y} [has_add A] [has_zero A] :
A → A

The scalar multiplication in an additive monoid. n •ℕ a = a+a+...+a n times.

Equations
@[instance]
def monoid.has_pow {M : Type u} [monoid M] :

Equations
@[simp]
theorem monoid.pow_eq_has_pow {M : Type u} [monoid M] (a : M) (n : ) :
monoid.pow a n = a ^ n

Commutativity

First we prove some facts about semiconj_by and commute. They do not require any theory about pow and/or nsmul and will be useful later in this file.

@[simp]
theorem semiconj_by.pow_right {M : Type u} [monoid M] {a x y : M} (h : semiconj_by a x y) (n : ) :
semiconj_by a (x ^ n) (y ^ n)

@[simp]
theorem commute.pow_right {M : Type u} [monoid M] {a b : M} (h : commute a b) (n : ) :
commute a (b ^ n)

@[simp]
theorem commute.pow_left {M : Type u} [monoid M] {a b : M} (h : commute a b) (n : ) :
commute (a ^ n) b

@[simp]
theorem commute.pow_pow {M : Type u} [monoid M] {a b : M} (h : commute a b) (m n : ) :
commute (a ^ m) (b ^ n)

@[simp]
theorem commute.self_pow {M : Type u} [monoid M] (a : M) (n : ) :
commute a (a ^ n)

@[simp]
theorem commute.pow_self {M : Type u} [monoid M] (a : M) (n : ) :
commute (a ^ n) a

@[simp]
theorem commute.pow_pow_self {M : Type u} [monoid M] (a : M) (m n : ) :
commute (a ^ m) (a ^ n)

@[simp]
theorem pow_zero {M : Type u} [monoid M] (a : M) :
a ^ 0 = 1

@[simp]
theorem zero_nsmul {A : Type y} [add_monoid A] (a : A) :
0 •ℕ a = 0

theorem pow_succ {M : Type u} [monoid M] (a : M) (n : ) :
a ^ (n + 1) = a * a ^ n

theorem succ_nsmul {A : Type y} [add_monoid A] (a : A) (n : ) :
(n + 1) •ℕ a = a + n •ℕ a

theorem pow_two {M : Type u} [monoid M] (a : M) :
a ^ 2 = a * a

theorem two_nsmul {A : Type y} [add_monoid A] (a : A) :
2 •ℕ a = a + a

theorem pow_mul_comm' {M : Type u} [monoid M] (a : M) (n : ) :
(a ^ n) * a = a * a ^ n

theorem nsmul_add_comm' {A : Type y} [add_monoid A] (a : A) (n : ) :
n •ℕ a + a = a + n •ℕ a

theorem pow_succ' {M : Type u} [monoid M] (a : M) (n : ) :
a ^ (n + 1) = (a ^ n) * a

theorem succ_nsmul' {A : Type y} [add_monoid A] (a : A) (n : ) :
(n + 1) •ℕ a = n •ℕ a + a

theorem pow_add {M : Type u} [monoid M] (a : M) (m n : ) :
a ^ (m + n) = (a ^ m) * a ^ n

theorem add_nsmul {A : Type y} [add_monoid A] (a : A) (m n : ) :
(m + n) •ℕ a = m •ℕ a + n •ℕ a

@[simp]
theorem pow_one {M : Type u} [monoid M] (a : M) :
a ^ 1 = a

@[simp]
theorem one_nsmul {A : Type y} [add_monoid A] (a : A) :
1 •ℕ a = a

@[simp]
theorem pow_ite {M : Type u} [monoid M] (P : Prop) [decidable P] (a : M) (b c : ) :
a ^ ite P b c = ite P (a ^ b) (a ^ c)

@[simp]
theorem ite_pow {M : Type u} [monoid M] (P : Prop) [decidable P] (a b : M) (c : ) :
ite P a b ^ c = ite P (a ^ c) (b ^ c)

@[simp]
theorem pow_boole {M : Type u} [monoid M] (P : Prop) [decidable P] (a : M) :
a ^ ite P 1 0 = ite P a 1

@[simp]
theorem one_pow {M : Type u} [monoid M] (n : ) :
1 ^ n = 1

@[simp]
theorem nsmul_zero {A : Type y} [add_monoid A] (n : ) :
n •ℕ 0 = 0

theorem pow_mul {M : Type u} [monoid M] (a : M) (m n : ) :
a ^ m * n = (a ^ m) ^ n

theorem mul_nsmul' {A : Type y} [add_monoid A] (a : A) (m n : ) :
m * n •ℕ a = n •ℕ (m •ℕ a)

theorem pow_mul' {M : Type u} [monoid M] (a : M) (m n : ) :
a ^ m * n = (a ^ n) ^ m

theorem mul_nsmul {A : Type y} [add_monoid A] (a : A) (m n : ) :
m * n •ℕ a = m •ℕ (n •ℕ a)

theorem pow_mul_pow_sub {M : Type u} [monoid M] (a : M) {m n : } :
m n(a ^ m) * a ^ (n - m) = a ^ n

theorem nsmul_add_sub_nsmul {A : Type y} [add_monoid A] (a : A) {m n : } :
m nm •ℕ a + (n - m) •ℕ a = n •ℕ a

theorem pow_sub_mul_pow {M : Type u} [monoid M] (a : M) {m n : } :
m n(a ^ (n - m)) * a ^ m = a ^ n

theorem sub_nsmul_nsmul_add {A : Type y} [add_monoid A] (a : A) {m n : } :
m n(n - m) •ℕ a + m •ℕ a = n •ℕ a

theorem pow_bit0 {M : Type u} [monoid M] (a : M) (n : ) :
a ^ bit0 n = (a ^ n) * a ^ n

theorem bit0_nsmul {A : Type y} [add_monoid A] (a : A) (n : ) :
bit0 n •ℕ a = n •ℕ a + n •ℕ a

theorem pow_bit1 {M : Type u} [monoid M] (a : M) (n : ) :
a ^ bit1 n = ((a ^ n) * a ^ n) * a

theorem bit1_nsmul {A : Type y} [add_monoid A] (a : A) (n : ) :
bit1 n •ℕ a = n •ℕ a + n •ℕ a + a

theorem pow_mul_comm {M : Type u} [monoid M] (a : M) (m n : ) :
(a ^ m) * a ^ n = (a ^ n) * a ^ m

theorem nsmul_add_comm {A : Type y} [add_monoid A] (a : A) (m n : ) :
m •ℕ a + n •ℕ a = n •ℕ a + m •ℕ a

theorem monoid_hom.map_pow {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M →* N) (a : M) (n : ) :
f (a ^ n) = f a ^ n

theorem add_monoid_hom.map_nsmul {A : Type y} {B : Type z} [add_monoid A] [add_monoid B] (f : A →+ B) (a : A) (n : ) :
f (n •ℕ a) = n •ℕ f a

theorem is_monoid_hom.map_pow {M : Type u} {N : Type v} [monoid M] [monoid N] (f : M → N) [is_monoid_hom f] (a : M) (n : ) :
f (a ^ n) = f a ^ n

theorem is_add_monoid_hom.map_nsmul {A : Type y} {B : Type z} [add_monoid A] [add_monoid B] (f : A → B) [is_add_monoid_hom f] (a : A) (n : ) :
f (n •ℕ a) = n •ℕ f a

theorem commute.mul_pow {M : Type u} [monoid M] {a b : M} (h : commute a b) (n : ) :
(a * b) ^ n = (a ^ n) * b ^ n

theorem neg_pow {R : Type u₁} [ring R] (a : R) (n : ) :
(-a) ^ n = ((-1) ^ n) * a ^ n

theorem pow_bit0' {M : Type u} [monoid M] (a : M) (n : ) :
a ^ bit0 n = (a * a) ^ n

theorem bit0_nsmul' {A : Type y} [add_monoid A] (a : A) (n : ) :
bit0 n •ℕ a = n •ℕ (a + a)

theorem pow_bit1' {M : Type u} [monoid M] (a : M) (n : ) :
a ^ bit1 n = ((a * a) ^ n) * a

theorem bit1_nsmul' {A : Type y} [add_monoid A] (a : A) (n : ) :
bit1 n •ℕ a = n •ℕ (a + a) + a

@[simp]
theorem neg_pow_bit0 {R : Type u₁} [ring R] (a : R) (n : ) :
(-a) ^ bit0 n = a ^ bit0 n

@[simp]
theorem neg_pow_bit1 {R : Type u₁} [ring R] (a : R) (n : ) :
(-a) ^ bit1 n = -a ^ bit1 n

Commutative (additive) monoid

theorem mul_pow {M : Type u} [comm_monoid M] (a b : M) (n : ) :
(a * b) ^ n = (a ^ n) * b ^ n

theorem nsmul_add {A : Type y} [add_comm_monoid A] (a b : A) (n : ) :
n •ℕ (a + b) = n •ℕ a + n •ℕ b

@[instance]
def pow.is_monoid_hom {M : Type u} [comm_monoid M] (n : ) :
is_monoid_hom (λ (_x : M), _x ^ n)

@[instance]

theorem dvd_pow {M : Type u} [comm_monoid M] {x y : M} {n : } :
x yn 0x y ^ n

def gpow {G : Type w} [group G] :
G → → G

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

Equations
def gsmul {A : Type y} [add_group A] :
A → A

The scalar multiplication by integers on an additive group. This extends nsmul to negative integers with the definition (-n) •ℤ a = -(n •ℕ a).

Equations
@[instance]
def group.has_pow {G : Type w} [group G] :

Equations
@[simp]
theorem group.gpow_eq_has_pow {G : Type w} [group G] (a : G) (n : ) :
gpow a n = a ^ n

@[simp]
theorem inv_pow {G : Type w} [group G] (a : G) (n : ) :
a⁻¹ ^ n = (a ^ n)⁻¹

@[simp]
theorem neg_nsmul {A : Type y} [add_group A] (a : A) (n : ) :
n •ℕ -a = -(n •ℕ a)

theorem pow_sub {G : Type w} [group G] (a : G) {m n : } :
n ma ^ (m - n) = (a ^ m) * (a ^ n)⁻¹

theorem nsmul_sub {A : Type y} [add_group A] (a : A) {m n : } :
n m(m - n) •ℕ a = m •ℕ a - n •ℕ a

theorem pow_inv_comm {G : Type w} [group G] (a : G) (m n : ) :
(a⁻¹ ^ m) * a ^ n = (a ^ n) * a⁻¹ ^ m

theorem nsmul_neg_comm {A : Type y} [add_group A] (a : A) (m n : ) :
m •ℕ -a + n •ℕ a = n •ℕ a + m •ℕ -a

@[simp]
theorem gpow_coe_nat {G : Type w} [group G] (a : G) (n : ) :
a ^ n = a ^ n

@[simp]
theorem gsmul_coe_nat {A : Type y} [add_group A] (a : A) (n : ) :

theorem gpow_of_nat {G : Type w} [group G] (a : G) (n : ) :
a ^ int.of_nat n = a ^ n

theorem gsmul_of_nat {A : Type y} [add_group A] (a : A) (n : ) :

@[simp]
theorem gpow_neg_succ_of_nat {G : Type w} [group G] (a : G) (n : ) :
a ^ -[1+ n] = (a ^ n.succ)⁻¹

@[simp]
theorem gsmul_neg_succ_of_nat {A : Type y} [add_group A] (a : A) (n : ) :

@[simp]
theorem gpow_zero {G : Type w} [group G] (a : G) :
a ^ 0 = 1

@[simp]
theorem zero_gsmul {A : Type y} [add_group A] (a : A) :
0 •ℤ a = 0

@[simp]
theorem gpow_one {G : Type w} [group G] (a : G) :
a ^ 1 = a

@[simp]
theorem one_gsmul {A : Type y} [add_group A] (a : A) :
1 •ℤ a = a

@[simp]
theorem one_gpow {G : Type w} [group G] (n : ) :
1 ^ n = 1

@[simp]
theorem gsmul_zero {A : Type y} [add_group A] (n : ) :
n •ℤ 0 = 0

@[simp]
theorem gpow_neg {G : Type w} [group G] (a : G) (n : ) :
a ^ -n = (a ^ n)⁻¹

theorem mul_gpow_neg_one {G : Type w} [group G] (a b : G) :
(a * b) ^ -1 = (b ^ -1) * a ^ -1

@[simp]
theorem neg_gsmul {A : Type y} [add_group A] (a : A) (n : ) :
-n •ℤ a = -(n •ℤ a)

theorem gpow_neg_one {G : Type w} [group G] (x : G) :
x ^ -1 = x⁻¹

theorem neg_one_gsmul {A : Type y} [add_group A] (x : A) :
(-1) •ℤ x = -x

theorem inv_gpow {G : Type w} [group G] (a : G) (n : ) :
a⁻¹ ^ n = (a ^ n)⁻¹

theorem gsmul_neg {A : Type y} [add_group A] (a : A) (n : ) :
n •ℤ -a = -(n •ℤ a)

theorem commute.mul_gpow {G : Type w} [group G] {a b : G} (h : commute a b) (n : ) :
(a * b) ^ n = (a ^ n) * b ^ n

theorem mul_gpow {G : Type w} [comm_group G] (a b : G) (n : ) :
(a * b) ^ n = (a ^ n) * b ^ n

theorem gsmul_add {A : Type y} [add_comm_group A] (a b : A) (n : ) :
n •ℤ (a + b) = n •ℤ a + n •ℤ b

theorem gsmul_sub {A : Type y} [add_comm_group A] (a b : A) (n : ) :
n •ℤ (a - b) = n •ℤ a - n •ℤ b

@[instance]
def gpow.is_group_hom {G : Type w} [comm_group G] (n : ) :
is_group_hom (λ (_x : G), _x ^ n)

@[instance]
def gsmul.is_add_group_hom {A : Type y} [add_comm_group A] (n : ) :

theorem zero_pow {R : Type u₁} [monoid_with_zero R] {n : } :
0 < n0 ^ n = 0

@[simp]
theorem ring_hom.map_pow {R : Type u₁} {S : Type u₂} [semiring R] [semiring S] (f : R →+* S) (a : R) (n : ) :
f (a ^ n) = f a ^ n

theorem neg_one_pow_eq_or {R : Type u₁} [ring R] (n : ) :
(-1) ^ n = 1 (-1) ^ n = -1

theorem pow_dvd_pow {R : Type u₁} [monoid R] (a : R) {m n : } :
m na ^ m a ^ n

theorem pow_dvd_pow_of_dvd {R : Type u₁} [comm_monoid R] {a b : R} (h : a b) (n : ) :
a ^ n b ^ n

theorem pow_two_sub_pow_two {R : Type u_1} [comm_ring R] (a b : R) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

theorem eq_or_eq_neg_of_pow_two_eq_pow_two {R : Type u₁} [integral_domain R] (a b : R) :
a ^ 2 = b ^ 2a = b a = -b

theorem sq_sub_sq {R : Type u₁} [comm_ring R] (a b : R) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

theorem pow_eq_zero {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {x : R} {n : } :
x ^ n = 0x = 0

@[simp]
theorem pow_eq_zero_iff {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {a : R} {n : } :
0 < n(a ^ n = 0 a = 0)

theorem pow_ne_zero {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {a : R} (n : ) :
a 0a ^ n 0

theorem pow_abs {R : Type u₁} [decidable_linear_ordered_comm_ring R] (a : R) (n : ) :
abs a ^ n = abs (a ^ n)

theorem abs_neg_one_pow {R : Type u₁} [decidable_linear_ordered_comm_ring R] (n : ) :
abs ((-1) ^ n) = 1

theorem nsmul_nonneg {A : Type y} [ordered_add_comm_monoid A] {a : A} (H : 0 a) (n : ) :
0 n •ℕ a

theorem nsmul_pos {A : Type y} [ordered_add_comm_monoid A] {a : A} (ha : 0 < a) {k : } :
0 < k0 < k •ℕ a

theorem nsmul_le_nsmul {A : Type y} [ordered_add_comm_monoid A] {a : A} {n m : } :
0 an mn •ℕ a m •ℕ a

theorem nsmul_le_nsmul_of_le_right {A : Type y} [ordered_add_comm_monoid A] {a b : A} (hab : a b) (i : ) :
i •ℕ a i •ℕ b

theorem gsmul_nonneg {A : Type y} [ordered_add_comm_group A] {a : A} (H : 0 a) {n : } :
0 n0 n •ℤ a

theorem nsmul_lt_nsmul {A : Type y} [ordered_cancel_add_comm_monoid A] {a : A} {n m : } :
0 < an < mn •ℕ a < m •ℕ a

theorem min_pow_dvd_add {R : Type u₁} [comm_semiring R] {n m : } {a b c : R} :
c ^ n ac ^ m bc ^ min n m a + b

theorem canonically_ordered_semiring.pow_pos {R : Type u₁} [canonically_ordered_comm_semiring R] {a : R} (H : 0 < a) (n : ) :
0 < a ^ n

theorem canonically_ordered_semiring.pow_le_pow_of_le_left {R : Type u₁} [canonically_ordered_comm_semiring R] {a b : R} (hab : a b) (i : ) :
a ^ i b ^ i

theorem canonically_ordered_semiring.one_le_pow_of_one_le {R : Type u₁} [canonically_ordered_comm_semiring R] {a : R} (H : 1 a) (n : ) :
1 a ^ n

theorem canonically_ordered_semiring.pow_le_one {R : Type u₁} [canonically_ordered_comm_semiring R] {a : R} (H : a 1) (n : ) :
a ^ n 1

@[simp]
theorem pow_pos {R : Type u₁} [linear_ordered_semiring R] {a : R} (H : 0 < a) (n : ) :
0 < a ^ n

@[simp]
theorem pow_nonneg {R : Type u₁} [linear_ordered_semiring R] {a : R} (H : 0 a) (n : ) :
0 a ^ n

theorem pow_lt_pow_of_lt_left {R : Type u₁} [linear_ordered_semiring R] {x y : R} {n : } :
x < y0 x0 < nx ^ n < y ^ n

theorem pow_left_inj {R : Type u₁} [linear_ordered_semiring R] {x y : R} {n : } :
0 x0 y0 < nx ^ n = y ^ nx = y

theorem one_le_pow_of_one_le {R : Type u₁} [linear_ordered_semiring R] {a : R} (H : 1 a) (n : ) :
1 a ^ n

theorem pow_le_pow {R : Type u₁} [linear_ordered_semiring R] {a : R} {n m : } :
1 an ma ^ n a ^ m

theorem pow_lt_pow {R : Type u₁} [linear_ordered_semiring R] {a : R} {n m : } :
1 < an < ma ^ n < a ^ m

theorem pow_le_pow_of_le_left {R : Type u₁} [linear_ordered_semiring R] {a b : R} (ha : 0 a) (hab : a b) (i : ) :
a ^ i b ^ i

theorem lt_of_pow_lt_pow {R : Type u₁} [linear_ordered_semiring R] {a b : R} (n : ) :
0 ba ^ n < b ^ na < b

theorem pow_two_nonneg {R : Type u₁} [linear_ordered_ring R] (a : R) :
0 a ^ 2

theorem pow_two_pos_of_ne_zero {R : Type u₁} [linear_ordered_ring R] (a : R) :
a 00 < a ^ 2

@[simp]
theorem neg_square {α : Type u_1} [ring α] (z : α) :
(-z) ^ 2 = z ^ 2

theorem of_add_nsmul {A : Type y} [add_monoid A] (x : A) (n : ) :

theorem of_add_gsmul {A : Type y} [add_group A] (x : A) (n : ) :

@[simp]
theorem semiconj_by.gpow_right {G : Type w} [group G] {a x y : G} (h : semiconj_by a x y) (m : ) :
semiconj_by a (x ^ m) (y ^ m)

@[simp]
theorem commute.gpow_right {G : Type w} [group G] {a b : G} (h : commute a b) (m : ) :
commute a (b ^ m)

@[simp]
theorem commute.gpow_left {G : Type w} [group G] {a b : G} (h : commute a b) (m : ) :
commute (a ^ m) b

theorem commute.gpow_gpow {G : Type w} [group G] {a b : G} (h : commute a b) (m n : ) :
commute (a ^ m) (b ^ n)

@[simp]
theorem commute.self_gpow {G : Type w} [group G] (a : G) (n : ) :
commute a (a ^ n)

@[simp]
theorem commute.gpow_self {G : Type w} [group G] (a : G) (n : ) :
commute (a ^ n) a

@[simp]
theorem commute.gpow_gpow_self {G : Type w} [group G] (a : G) (m n : ) :
commute (a ^ m) (a ^ n)