mathlib3 documentation

algebra.group_power.basic

Power operations on monoids and groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 lemmas about a ^ n and n • a, where n : ℕ or n : ℤ. Further lemmas can be found in algebra.group_power.lemmas.

The analogous results for groups with zero can be found in algebra.group_with_zero.power.

Notation #

a ^ n is used as notation for has_pow.pow a n; in this file n : ℕ or n : ℤ.
n • a is used as notation for has_smul.smul n a; in this file n : ℕ or n : ℤ.

Implementation details #

We adopt the convention that 0^0 = 1.

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 pow_ite {M : Type u} [has_pow 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} [has_pow M ℕ] (P : Prop) [decidable P] (a b : M) (c : ℕ) :

ite P a b ^ c = ite P (a ^ c) (b ^ c)

@[simp]

theorem pow_one {M : Type u} [monoid M] (a : M) :

a ^ 1 = a

@[simp]

theorem one_nsmul {M : Type u} [add_monoid M] (a : M) :

1 • a = a

@[nolint]

theorem pow_two {M : Type u} [monoid M] (a : M) :

a ^ 2 = a * a

Note that most of the lemmas about powers of two refer to it as sq.

theorem two_nsmul {M : Type u} [add_monoid M] (a : M) :

2 • a = a + a

theorem sq {M : Type u} [monoid M] (a : M) :

a ^ 2 = a * a

Alias of pow_two.

theorem pow_three' {M : Type u} [monoid M] (a : M) :

a ^ 3 = a * a * a

theorem pow_three {M : Type u} [monoid M] (a : M) :

a ^ 3 = a * (a * a)

theorem nsmul_add_comm' {M : Type u} [add_monoid M] (a : M) (n : ℕ) :

n • a + a = a + n • a

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

a ^ n * a = a * a ^ n

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

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

theorem add_nsmul {M : Type u} [add_monoid M] (a : M) (m n : ℕ) :

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

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

theorem nsmul_zero {M : Type u} [add_monoid M] (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' {M : Type u} [add_monoid M] (a : M) (m n : ℕ) :

(m * n) • a = n • m • a

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

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

theorem nsmul_left_comm {M : Type u} [add_monoid M] (a : M) (m n : ℕ) :

n • m • a = m • n • a

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

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

theorem mul_nsmul {M : Type u} [add_monoid M] (a : M) (m n : ℕ) :

(m * n) • a = m • n • a

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

m • a + (n - m) • a = 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 sub_nsmul_nsmul_add {M : Type u} [add_monoid M] (a : M) {m n : ℕ} (h : m ≤ n) :

(n - m) • a + 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 pow_eq_pow_mod {M : Type u_1} [monoid M] {x : M} (m : ℕ) {n : ℕ} (h : x ^ n = 1) :

x ^ m = x ^ (m % n)

If x ^ n = 1, then x ^ m is the same as x ^ (m % n)

theorem nsmul_eq_mod_nsmul {M : Type u_1} [add_monoid M] {x : M} (m : ℕ) {n : ℕ} (h : n • x = 0) :

m • x = (m % n) • x

If n • x = 0, then m • x is the same as (m % n) • x

theorem bit0_nsmul {M : Type u} [add_monoid M] (a : M) (n : ℕ) :

bit0 n • a = n • a + n • a

theorem pow_bit0 {M : Type u} [monoid M] (a : M) (n : ℕ) :

a ^ bit0 n = a ^ n * a ^ n

theorem bit1_nsmul {M : Type u} [add_monoid M] (a : M) (n : ℕ) :

bit1 n • a = n • a + n • a + a

theorem pow_bit1 {M : Type u} [monoid M] (a : M) (n : ℕ) :

a ^ bit1 n = a ^ n * a ^ n * a

theorem nsmul_add_comm {M : Type u} [add_monoid M] (a : M) (m n : ℕ) :

m • a + n • a = n • a + m • a

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

a ^ m * a ^ n = a ^ n * a ^ m

theorem add_commute.add_nsmul {M : Type u} [add_monoid M] {a b : M} (h : add_commute a b) (n : ℕ) :

n • (a + b) = n • a + n • b

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 bit0_nsmul' {M : Type u} [add_monoid M] (a : M) (n : ℕ) :

bit0 n • a = n • (a + a)

theorem pow_bit0' {M : Type u} [monoid M] (a : M) (n : ℕ) :

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

theorem bit1_nsmul' {M : Type u} [add_monoid M] (a : M) (n : ℕ) :

bit1 n • a = n • (a + a) + a

theorem pow_bit1' {M : Type u} [monoid M] (a : M) (n : ℕ) :

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

theorem nsmul_add_nsmul_eq_zero {M : Type u} [add_monoid M] {a b : M} (n : ℕ) (h : a + b = 0) :

n • a + n • b = 0

theorem pow_mul_pow_eq_one {M : Type u} [monoid M] {a b : M} (n : ℕ) (h : a * b = 1) :

a ^ n * b ^ n = 1

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

x ∣ y ^ n

theorem has_dvd.dvd.pow {M : Type u} [monoid M] {x y : M} (hxy : x ∣ y) {n : ℕ} (hn : n ≠ 0) :

x ∣ y ^ n

Alias of dvd_pow.

theorem dvd_pow_self {M : Type u} [monoid M] (a : M) {n : ℕ} (hn : n ≠ 0) :

a ∣ a ^ n

Commutative (additive) monoid #

theorem nsmul_add {M : Type u} [add_comm_monoid M] (a b : M) (n : ℕ) :

n • (a + b) = n • a + n • b

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

(a * b) ^ n = a ^ n * b ^ n

@[simp]

theorem nsmul_add_monoid_hom_apply {M : Type u} [add_comm_monoid M] (n : ℕ) (_x : M) :

⇑(nsmul_add_monoid_hom n) _x = n • _x

def nsmul_add_monoid_hom {M : Type u} [add_comm_monoid M] (n : ℕ) :

M →+ M

Multiplication by a natural n on a commutative additive monoid, considered as a morphism of additive monoids.

Equations

nsmul_add_monoid_hom n = {to_fun := λ (_x : M), n • _x, map_zero' := _, map_add' := _}

def pow_monoid_hom {M : Type u} [comm_monoid M] (n : ℕ) :

M →* M

The nth power map on a commutative monoid for a natural n, considered as a morphism of monoids.

Equations

pow_monoid_hom n = {to_fun := λ (_x : M), _x ^ n, map_one' := _, map_mul' := _}

@[simp]

theorem pow_monoid_hom_apply {M : Type u} [comm_monoid M] (n : ℕ) (_x : M) :

⇑(pow_monoid_hom n) _x = _x ^ n

@[simp]

theorem zpow_one {G : Type w} [div_inv_monoid G] (a : G) :

a ^ 1 = a

@[simp]

theorem one_zsmul {G : Type w} [sub_neg_monoid G] (a : G) :

1 • a = a

theorem zpow_two {G : Type w} [div_inv_monoid G] (a : G) :

a ^ 2 = a * a

theorem two_zsmul {G : Type w} [sub_neg_monoid G] (a : G) :

2 • a = a + a

theorem zpow_neg_one {G : Type w} [div_inv_monoid G] (x : G) :

x ^ -1 = x⁻¹

theorem neg_one_zsmul {G : Type w} [sub_neg_monoid G] (x : G) :

(-1) • x = -x

theorem zsmul_neg_coe_of_pos {G : Type w} [sub_neg_monoid G] (a : G) {n : ℕ} :

0 < n → -↑n • a = -(n • a)

theorem zpow_neg_coe_of_pos {G : Type w} [div_inv_monoid G] (a : G) {n : ℕ} :

0 < n → a ^ -↑n = (a ^ n)⁻¹

@[simp]

theorem inv_pow {α : Type u_1} [division_monoid α] (a : α) (n : ℕ) :

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

@[simp]

theorem neg_nsmul {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℕ) :

n • -a = -(n • a)

theorem zsmul_zero {α : Type u_1} [subtraction_monoid α] (n : ℤ) :

n • 0 = 0

@[simp]

theorem one_zpow {α : Type u_1} [division_monoid α] (n : ℤ) :

1 ^ n = 1

@[simp]

theorem neg_zsmul {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℤ) :

-n • a = -(n • a)

@[simp]

theorem zpow_neg {α : Type u_1} [division_monoid α] (a : α) (n : ℤ) :

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

theorem mul_zpow_neg_one {α : Type u_1} [division_monoid α] (a b : α) :

(a * b) ^ -1 = b ^ -1 * a ^ -1

theorem neg_one_zsmul_add {α : Type u_1} [subtraction_monoid α] (a b : α) :

(-1) • (a + b) = (-1) • b + (-1) • a

theorem zsmul_neg {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℤ) :

n • -a = -(n • a)

theorem inv_zpow {α : Type u_1} [division_monoid α] (a : α) (n : ℤ) :

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

@[simp]

theorem zsmul_neg' {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℤ) :

n • -a = -n • a

@[simp]

theorem inv_zpow' {α : Type u_1} [division_monoid α] (a : α) (n : ℤ) :

a⁻¹ ^ n = a ^ -n

theorem nsmul_zero_sub {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℕ) :

n • (0 - a) = 0 - n • a

theorem one_div_pow {α : Type u_1} [division_monoid α] (a : α) (n : ℕ) :

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

theorem zsmul_zero_sub {α : Type u_1} [subtraction_monoid α] (a : α) (n : ℤ) :

n • (0 - a) = 0 - n • a

theorem one_div_zpow {α : Type u_1} [division_monoid α] (a : α) (n : ℤ) :

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

@[protected]

theorem commute.mul_zpow {α : Type u_1} [division_monoid α] {a b : α} (h : commute a b) (i : ℤ) :

(a * b) ^ i = a ^ i * b ^ i

@[protected]

theorem add_commute.zsmul_add {α : Type u_1} [subtraction_monoid α] {a b : α} (h : add_commute a b) (i : ℤ) :

i • (a + b) = i • a + i • b

theorem zsmul_add {α : Type u_1} [subtraction_comm_monoid α] (a b : α) (n : ℤ) :

n • (a + b) = n • a + n • b

theorem mul_zpow {α : Type u_1} [division_comm_monoid α] (a b : α) (n : ℤ) :

(a * b) ^ n = a ^ n * b ^ n

@[simp]

theorem div_pow {α : Type u_1} [division_comm_monoid α] (a b : α) (n : ℕ) :

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

@[simp]

theorem nsmul_sub {α : Type u_1} [subtraction_comm_monoid α] (a b : α) (n : ℕ) :

n • (a - b) = n • a - n • b

@[simp]

theorem zsmul_sub {α : Type u_1} [subtraction_comm_monoid α] (a b : α) (n : ℤ) :

n • (a - b) = n • a - n • b

@[simp]

theorem div_zpow {α : Type u_1} [division_comm_monoid α] (a b : α) (n : ℤ) :

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

@[simp]

theorem zpow_group_hom_apply {α : Type u_1} [division_comm_monoid α] (n : ℤ) (_x : α) :

⇑(zpow_group_hom n) _x = _x ^ n

def zpow_group_hom {α : Type u_1} [division_comm_monoid α] (n : ℤ) :

α →* α

The n-th power map (for an integer n) on a commutative group, considered as a group homomorphism.

Equations

zpow_group_hom n = {to_fun := λ (_x : α), _x ^ n, map_one' := _, map_mul' := _}

def zsmul_add_group_hom {α : Type u_1} [subtraction_comm_monoid α] (n : ℤ) :

α →+ α

Multiplication by an integer n on a commutative additive group, considered as an additive group homomorphism.

Equations

zsmul_add_group_hom n = {to_fun := λ (_x : α), n • _x, map_zero' := _, map_add' := _}

@[simp]

theorem zsmul_add_group_hom_apply {α : Type u_1} [subtraction_comm_monoid α] (n : ℤ) (_x : α) :

⇑(zsmul_add_group_hom n) _x = n • _x

theorem sub_nsmul {G : Type w} [add_group G] (a : G) {m n : ℕ} (h : n ≤ m) :

(m - n) • a = m • 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 pow_inv_comm {G : Type w} [group G] (a : G) (m n : ℕ) :

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

theorem nsmul_neg_comm {G : Type w} [add_group G] (a : G) (m n : ℕ) :

m • -a + n • a = n • a + m • -a

theorem sub_nsmul_neg {G : Type w} [add_group G] (a : G) {m n : ℕ} (h : n ≤ m) :

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

theorem inv_pow_sub {G : Type w} [group G] (a : G) {m n : ℕ} (h : n ≤ m) :

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

theorem pow_dvd_pow {R : Type u₁} [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) :

a ^ m ∣ a ^ n

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_zsmul {A : Type y} [sub_neg_monoid A] (x : A) (n : ℤ) :

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

theorem of_mul_pow {A : Type y} [monoid A] (x : A) (n : ℕ) :

⇑additive.of_mul (x ^ n) = n • ⇑additive.of_mul x

theorem of_mul_zpow {G : Type w} [div_inv_monoid G] (x : G) (n : ℤ) :

⇑additive.of_mul (x ^ n) = n • ⇑additive.of_mul x

@[simp]

theorem add_semiconj_by.zsmul_right {G : Type w} [add_group G] {a x y : G} (h : add_semiconj_by a x y) (m : ℤ) :

add_semiconj_by a (m • x) (m • y)

@[simp]

theorem semiconj_by.zpow_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 add_commute.zsmul_right {G : Type w} [add_group G] {a b : G} (h : add_commute a b) (m : ℤ) :

add_commute a (m • b)

@[simp]

theorem commute.zpow_right {G : Type w} [group G] {a b : G} (h : commute a b) (m : ℤ) :

commute a (b ^ m)

@[simp]

theorem commute.zpow_left {G : Type w} [group G] {a b : G} (h : commute a b) (m : ℤ) :

commute (a ^ m) b

@[simp]

theorem add_commute.zsmul_left {G : Type w} [add_group G] {a b : G} (h : add_commute a b) (m : ℤ) :

add_commute (m • a) b

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

commute (a ^ m) (b ^ n)

theorem add_commute.zsmul_zsmul {G : Type w} [add_group G] {a b : G} (h : add_commute a b) (m n : ℤ) :

add_commute (m • a) (n • b)

@[simp]

theorem commute.self_zpow {G : Type w} [group G] (a : G) (n : ℤ) :

commute a (a ^ n)

@[simp]

theorem add_commute.self_zsmul {G : Type w} [add_group G] (a : G) (n : ℤ) :

add_commute a (n • a)

@[simp]

theorem commute.zpow_self {G : Type w} [group G] (a : G) (n : ℤ) :

commute (a ^ n) a

@[simp]

theorem add_commute.zsmul_self {G : Type w} [add_group G] (a : G) (n : ℤ) :

add_commute (n • a) a

@[simp]

theorem commute.zpow_zpow_self {G : Type w} [group G] (a : G) (m n : ℤ) :

commute (a ^ m) (a ^ n)

@[simp]

theorem add_commute.zsmul_zsmul_self {G : Type w} [add_group G] (a : G) (m n : ℤ) :

add_commute (m • a) (n • a)