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] (a : M) (a_1 : ℕ) :

M

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

Equations

monoid.pow a (n + 1) = a * monoid.pow a n
monoid.pow a 0 = 1

def nsmul {A : Type y} [has_add A] [has_zero A] (n : ℕ) (a : A) :

A

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

Equations

n •ℕ a = monoid.pow a n

@[instance]

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

Equations

monoid.has_pow = {pow := monoid.pow (monoid.to_has_one M)}

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 : ℕ} (h : m ≤ n) :

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

theorem nsmul_add_sub_nsmul {A : Type y} [add_monoid A] (a : A) {m n : ℕ} (h : m ≤ n) :

m •ℕ a + (n - m) •ℕ a = n •ℕ a

theorem pow_sub_mul_pow {M : Type u} [monoid M] (a : M) {m n : ℕ} (h : m ≤ n) :

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

theorem sub_nsmul_nsmul_add {A : Type y} [add_monoid A] (a : A) {m n : ℕ} (h : 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

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]

def nsmul.is_add_monoid_hom {A : Type y} [add_comm_monoid A] (n : ℕ) :

is_add_monoid_hom (nsmul n)

theorem dvd_pow {M : Type u} [comm_monoid M] {x y : M} {n : ℕ} (hxy : x ∣ y) (hn : n ≠ 0) :

x ∣ y ^ n

def gpow {G : Type w} [group G] (a : G) (a_1 : ℤ) :

G

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

Equations

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

def gsmul {A : Type y} [add_group A] (n : ℤ) (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

n •ℤ a = gpow a n

@[instance]

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

Equations

group.has_pow = {pow := gpow _inst_1}

@[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 : ℕ} (h : n ≤ m) :

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

theorem nsmul_sub {A : Type y} [add_group A] (a : A) {m n : ℕ} (a_1 : 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 : ℕ) :

↑n •ℤ a = n •ℕ a

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

int.of_nat n •ℤ a = n •ℕ a

@[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 : ℕ) :

-[1+ n] •ℤ a = -(n.succ •ℕ a)

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

is_add_group_hom (gsmul n)

theorem zero_pow {R : Type u₁} [monoid_with_zero R] {n : ℕ} (a : 0 < n) :

0 ^ 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 : ℕ} (h : m ≤ n) :

a ^ 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) (h : a ^ 2 = b ^ 2) :

a = 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 : ℕ} (H : x ^ n = 0) :

x = 0

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

a ^ n ≠ 0

theorem nsmul_nonneg {R : Type u₁} [ordered_add_comm_monoid R] {a : R} (H : 0 ≤ a) (n : ℕ) :

0 ≤ n •ℕ a

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_le_nsmul {A : Type y} [ordered_add_comm_monoid A] {a : A} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) :

n •ℕ 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 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

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

0 < a ^ n

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 : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) :

x ^ n < y ^ n

theorem pow_left_inj {R : Type u₁} [linear_ordered_semiring R] {x y : R} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) (Hxyn : x ^ n = y ^ n) :

x = 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 : ℕ} (ha : 1 ≤ a) (h : n ≤ m) :

a ^ n ≤ a ^ m

theorem pow_lt_pow {R : Type u₁} [linear_ordered_semiring R] {a : R} {n m : ℕ} (h : 1 < a) (h2 : n < m) :

a ^ 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 : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) :

a < 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) (h : a ≠ 0) :

0 < 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 : ℕ) :

multiplicative.of_add (n •ℕ x) = multiplicative.of_add x ^ n

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

multiplicative.of_add (n •ℤ x) = multiplicative.of_add x ^ 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)