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 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_scalar.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 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 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 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 {G : Type w} [group G] (a : G) (n : ℕ) :

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

@[simp]

theorem neg_nsmul {G : Type w} [add_group G] (a : G) (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 {G : Type w} [add_group G] (a : G) {m n : ℕ} (h : 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 {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 zsmul_zero {G : Type w} [add_group G] (n : ℤ) :

n • 0 = 0

@[simp]

theorem one_zpow {G : Type w} [group G] (n : ℤ) :

1 ^ n = 1

@[simp]

theorem neg_zsmul {G : Type w} [add_group G] (a : G) (n : ℤ) :

-n • a = -(n • a)

@[simp]

theorem zpow_neg {G : Type w} [group G] (a : G) (n : ℤ) :

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

theorem mul_zpow_neg_one {G : Type w} [group G] (a b : G) :

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

theorem neg_one_zsmul_add {G : Type w} [add_group G] (a b : G) :

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

theorem zsmul_neg {G : Type w} [add_group G] (a : G) (n : ℤ) :

n • -a = -(n • a)

theorem inv_zpow {G : Type w} [group G] (a : G) (n : ℤ) :

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

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

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

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

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

theorem zsmul_add {G : Type w} [add_comm_group G] (a b : G) (n : ℤ) :

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

theorem mul_zpow {G : Type w} [comm_group G] (a b : G) (n : ℤ) :

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

theorem zsmul_sub {G : Type w} [add_comm_group G] (a b : G) (n : ℤ) :

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

theorem div_zpow {G : Type w} [comm_group G] (a b : G) (n : ℤ) :

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

@[simp]

theorem zpow_group_hom_apply {G : Type w} [comm_group G] (n : ℤ) (_x : G) :

⇑(zpow_group_hom n) _x = _x ^ n

def zpow_group_hom {G : Type w} [comm_group G] (n : ℤ) :

G →* G

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

Equations

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

def zsmul_add_group_hom {G : Type w} [add_comm_group G] (n : ℤ) :

G →+ G

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 : G), n • _x, map_zero' := _, map_add' := _}

@[simp]

theorem zsmul_add_group_hom_apply {G : Type w} [add_comm_group G] (n : ℤ) (_x : G) :

⇑(zsmul_add_group_hom n) _x = n • _x

theorem zero_pow {R : Type u₁} [monoid_with_zero R] {n : ℕ} :

0 < n → 0 ^ n = 0

theorem zero_pow_eq {R : Type u₁} [monoid_with_zero R] (n : ℕ) :

0 ^ n = ite (n = 0) 1 0

theorem pow_eq_zero_of_le {M : Type u} [monoid_with_zero M] {x : M} {n m : ℕ} (hn : n ≤ m) (hx : x ^ n = 0) :

x ^ m = 0

@[protected]

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 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_eq_zero {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {x : R} {n : ℕ} (H : x ^ n = 0) :

x = 0

@[simp]

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

a ^ n = 0 ↔ a = 0

theorem pow_ne_zero_iff {R : Type u₁} [monoid_with_zero R] [no_zero_divisors R] {a : R} {n : ℕ} (hn : 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 : ℕ) (h : a ≠ 0) :

a ^ n ≠ 0

theorem pow_dvd_pow_iff {R : Type u₁} [cancel_comm_monoid_with_zero R] {x : R} {n m : ℕ} (h0 : x ≠ 0) (h1 : ¬is_unit x) :

x ^ n ∣ x ^ m ↔ n ≤ m

theorem min_pow_dvd_add {R : Type u₁} [semiring R] {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) :

c ^ min n m ∣ a + b

theorem add_sq {R : Type u₁} [comm_semiring R] (a b : R) :

(a + b) ^ 2 = a ^ 2 + (2 * a) * b + b ^ 2

theorem add_pow_two {R : Type u₁} [comm_semiring R] (a b : R) :

(a + b) ^ 2 = a ^ 2 + (2 * a) * b + b ^ 2

Alias of add_sq.

theorem neg_one_pow_eq_or (R : Type u₁) [monoid R] [has_distrib_neg R] (n : ℕ) :

(-1) ^ n = 1 ∨ (-1) ^ n = -1

theorem neg_pow {R : Type u₁} [monoid R] [has_distrib_neg R] (a : R) (n : ℕ) :

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

@[simp]

theorem neg_pow_bit0 {R : Type u₁} [monoid R] [has_distrib_neg R] (a : R) (n : ℕ) :

(-a) ^ bit0 n = a ^ bit0 n

@[simp]

theorem neg_pow_bit1 {R : Type u₁} [monoid R] [has_distrib_neg R] (a : R) (n : ℕ) :

(-a) ^ bit1 n = -a ^ bit1 n

@[simp]

theorem neg_sq {R : Type u₁} [monoid R] [has_distrib_neg R] (a : R) :

(-a) ^ 2 = a ^ 2

@[simp]

theorem neg_one_sq {R : Type u₁} [monoid R] [has_distrib_neg R] :

(-1) ^ 2 = 1

theorem neg_pow_two {R : Type u₁} [monoid R] [has_distrib_neg R] (a : R) :

(-a) ^ 2 = a ^ 2

Alias of neg_sq.

theorem neg_one_pow_two {R : Type u₁} [monoid R] [has_distrib_neg R] :

(-1) ^ 2 = 1

Alias of neg_one_sq.

@[simp]

theorem neg_one_pow_mul_eq_zero_iff {R : Type u₁} [ring R] {n : ℕ} {r : R} :

((-1) ^ n) * r = 0 ↔ r = 0

@[simp]

theorem mul_neg_one_pow_eq_zero_iff {R : Type u₁} [ring R] {n : ℕ} {r : R} :

r * (-1) ^ n = 0 ↔ r = 0

theorem sq_sub_sq {R : Type u₁} [comm_ring R] (a b : R) :

a ^ 2 - b ^ 2 = (a + b) * (a - b)

theorem pow_two_sub_pow_two {R : Type u₁} [comm_ring R] (a b : R) :

a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of sq_sub_sq.

theorem eq_or_eq_neg_of_sq_eq_sq {R : Type u₁} [comm_ring R] [no_zero_divisors R] (a b : R) (h : a ^ 2 = b ^ 2) :

a = b ∨ a = -b

theorem sub_sq {R : Type u₁} [comm_ring R] (a b : R) :

(a - b) ^ 2 = a ^ 2 - (2 * a) * b + b ^ 2

theorem sub_pow_two {R : Type u₁} [comm_ring R] (a b : R) :

(a - b) ^ 2 = a ^ 2 - (2 * a) * b + b ^ 2

Alias of sub_sq.

theorem units.eq_or_eq_neg_of_sq_eq_sq {R : Type u₁} [comm_ring R] [no_zero_divisors R] (a b : Rˣ) (h : a ^ 2 = b ^ 2) :

a = b ∨ a = -b

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

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

commute (a ^ m) (b ^ n)

@[simp]

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

commute a (a ^ n)

@[simp]

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

commute (a ^ n) a

@[simp]

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

commute (a ^ m) (a ^ n)