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.

Scalar multiplication by naturals and integers is handled by the (has_scalar.smul) notation defined elsewhere.

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.

@[instance]
def monoid.has_pow {M : Type u} [monoid M] :
Equations
@[instance]
Equations
@[instance]
def div_inv_monoid.has_pow {M : Type u} [div_inv_monoid M] :
Equations
@[instance]
Equations
@[simp]
theorem npow_eq_pow {M : Type u_1} [monoid M] (n : ) (x : M) :
npow n x = x ^ n
@[simp]
theorem nsmul_eq_smul {M : Type u_1} [add_monoid M] (n : ) (x : M) :
nsmul n x = n x
@[simp]
theorem gsmul_eq_smul {M : Type u_1} [sub_neg_monoid M] (n : ) (x : M) :
gsmul n x = n x
@[simp]
theorem gpow_eq_pow {M : Type u_1} [div_inv_monoid M] (n : ) (x : M) :
gpow n x = x ^ 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 add_semiconj_by.pow_right {M : Type u} [add_monoid M] {a x y : M} (h : add_semiconj_by a x y) (n : ) :
add_semiconj_by a (n x) (n y)
@[simp]
theorem add_commute.pow_right {M : Type u} [add_monoid M] {a b : M} (h : add_commute a b) (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 add_commute.pow_left {M : Type u} [add_monoid M] {a b : M} (h : add_commute a b) (n : ) :
@[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 add_commute.pow_pow {M : Type u} [add_monoid M] {a b : M} (h : add_commute a b) (m n : ) :
add_commute (m a) (n b)
@[simp]
theorem commute.self_pow {M : Type u} [monoid M] (a : M) (n : ) :
commute a (a ^ n)
@[simp]
theorem add_commute.self_pow {M : Type u} [add_monoid M] (a : M) (n : ) :
@[simp]
theorem commute.pow_self {M : Type u} [monoid M] (a : M) (n : ) :
commute (a ^ n) a
@[simp]
theorem add_commute.pow_self {M : Type u} [add_monoid M] (a : M) (n : ) :
@[simp]
theorem add_commute.pow_pow_self {M : Type u} [add_monoid M] (a : M) (m n : ) :
add_commute (m a) (n a)
@[simp]
theorem commute.pow_pow_self {M : Type u} [monoid M] (a : M) (m n : ) :
commute (a ^ m) (a ^ n)
theorem zero_nsmul {M : Type u} [add_monoid M] (a : M) :
0 a = 0
@[simp]
theorem pow_zero {M : Type u} [monoid M] (a : M) :
a ^ 0 = 1
theorem succ_nsmul {M : Type u} [add_monoid M] (a : M) (n : ) :
(n + 1) a = a + n a
theorem pow_succ {M : Type u} [monoid M] (a : M) (n : ) :
a ^ (n + 1) = a * a ^ n
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_succ' {M : Type u} [monoid M] (a : M) (n : ) :
a ^ (n + 1) = (a ^ n) * a
theorem succ_nsmul' {M : Type u} [add_monoid M] (a : M) (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 {M : Type u} [add_monoid M] (a : M) (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 {M : Type u} [add_monoid M] (a : M) :
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
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_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
@[simp]
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
@[simp]
theorem add_monoid_hom.map_nsmul {M : Type u} {N : Type v} [add_monoid M] [add_monoid N] (f : M →+ N) (a : M) (n : ) :
f (n a) = n f a
theorem add_commute.add_pow {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 neg_pow {R : Type u₁} [ring R] (a : R) (n : ) :
(-a) ^ n = ((-1) ^ n) * a ^ 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
@[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 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) :
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.

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
@[simp]
theorem pow_monoid_hom_apply {M : Type u} [comm_monoid M] (n : ) (_x : M) :
(pow_monoid_hom n) _x = _x ^ n
theorem dvd_pow {M : Type u} [comm_monoid M] {x y : M} (hxy : x y) {n : } (hn : n 0) :
x y ^ n
theorem has_dvd.dvd.pow {M : Type u} [comm_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} [comm_monoid M] (a : M) {n : } (hn : n 0) :
a a ^ n
@[simp]
theorem gsmul_coe_nat {G : Type w} [sub_neg_monoid G] (a : G) (n : ) :
n a = n a
@[simp]
theorem gpow_coe_nat {G : Type w} [div_inv_monoid G] (a : G) (n : ) :
a ^ n = a ^ n
theorem gpow_of_nat {G : Type w} [div_inv_monoid G] (a : G) (n : ) :
a ^ int.of_nat n = a ^ n
theorem gsmul_of_nat {G : Type w} [sub_neg_monoid G] (a : G) (n : ) :
@[simp]
theorem gsmul_neg_succ_of_nat {G : Type w} [sub_neg_monoid G] (a : G) (n : ) :
-[1+ n] a = -(n.succ a)
@[simp]
theorem gpow_neg_succ_of_nat {G : Type w} [div_inv_monoid G] (a : G) (n : ) :
a ^ -[1+ n] = (a ^ n.succ)⁻¹
@[simp]
theorem zero_gsmul {G : Type w} [sub_neg_monoid G] (a : G) :
0 a = 0
@[simp]
theorem gpow_zero {G : Type w} [div_inv_monoid G] (a : G) :
a ^ 0 = 1
@[simp]
theorem gpow_one {G : Type w} [div_inv_monoid G] (a : G) :
a ^ 1 = a
@[simp]
theorem one_gsmul {G : Type w} [sub_neg_monoid G] (a : G) :
1 a = a
@[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
@[simp]
theorem one_gpow {G : Type w} [group G] (n : ) :
1 ^ n = 1
@[simp]
theorem gsmul_zero {G : Type w} [add_group G] (n : ) :
n 0 = 0
@[simp]
theorem gpow_neg {G : Type w} [group G] (a : G) (n : ) :
a ^ -n = (a ^ n)⁻¹
@[simp]
theorem neg_gsmul {G : Type w} [add_group G] (a : G) (n : ) :
-n a = -(n a)
theorem mul_gpow_neg_one {G : Type w} [group G] (a b : G) :
(a * b) ^ -1 = (b ^ -1) * a ^ -1
theorem gpow_neg_one {G : Type w} [group G] (x : G) :
x ^ -1 = x⁻¹
theorem neg_one_gsmul {G : Type w} [add_group G] (x : G) :
(-1) x = -x
theorem gsmul_neg {G : Type w} [add_group G] (a : G) (n : ) :
n -a = -(n a)
theorem inv_gpow {G : Type w} [group G] (a : G) (n : ) :
a⁻¹ ^ n = (a ^ n)⁻¹
theorem add_commute.gsmul_add {G : Type w} [add_group G] {a b : G} (h : add_commute a b) (n : ) :
n (a + b) = n a + n b
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 {G : Type w} [add_comm_group G] (a b : G) (n : ) :
n (a + b) = n a + n b
theorem gsmul_sub {G : Type w} [add_comm_group G] (a b : G) (n : ) :
n (a - b) = n a - n b
theorem div_gpow {G : Type w} [comm_group G] (a b : G) (n : ) :
(a / b) ^ n = a ^ n / b ^ n
def gpow_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
def gsmul_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.

@[simp]
theorem gpow_group_hom_apply {G : Type w} [comm_group G] (n : ) (_x : G) :
(gpow_group_hom n) _x = _x ^ n
@[simp]
theorem gsmul_add_group_hom_apply {G : Type w} [add_comm_group G] (n : ) (_x : G) :
theorem zero_pow {R : Type u₁} [monoid_with_zero R] {n : } :
0 < n0 ^ 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
@[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
@[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 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 sq_sub_sq {R : Type u_1} [comm_ring R] (a b : R) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)
theorem pow_two_sub_pow_two {R : Type u_1} [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₁} [integral_domain R] (a b : R) (h : 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
@[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 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.

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

Alias of neg_sq.

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

Alias of sub_sq.

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 : ) :
theorem of_mul_pow {A : Type u_1} [monoid A] (x : A) (n : ) :
theorem of_mul_gpow {G : Type w} [group G] (x : G) (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)