# mathlibdocumentation

algebra.group_power.lemmas

# Lemmas about power operations on monoids and groups

This file contains lemmas about monoid.pow, group.pow, nsmul, gsmul which require additional imports besides those available in .basic.

@[simp]
theorem nsmul_one {A : Type y} [add_monoid A] [has_one A] (n : ) :
n •ℕ 1 = n

@[simp]
theorem list.prod_repeat {M : Type u} [monoid M] (a : M) (n : ) :
n).prod = a ^ n

@[simp]
theorem list.sum_repeat {A : Type y} [add_monoid A] (a : A) (n : ) :
n).sum = n •ℕ a

@[simp]
theorem units.coe_pow {M : Type u} [monoid M] (u : units M) (n : ) :
(u ^ n) = u ^ n

theorem is_unit_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ) :
x ^ n = 10 < n

theorem nat.nsmul_eq_mul (m n : ) :
m •ℕ n = m * n

theorem gsmul_one {A : Type y} [add_group A] [has_one A] (n : ) :
n •ℤ 1 = n

theorem gpow_add_one {G : Type w} [group G] (a : G) (n : ) :
a ^ (n + 1) = (a ^ n) * a

theorem add_one_gsmul {A : Type y} [add_group A] (a : A) (i : ) :
(i + 1) •ℤ a = i •ℤ a + a

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

theorem gpow_add {G : Type w} [group G] (a : G) (m n : ) :
a ^ (m + n) = (a ^ m) * a ^ n

theorem mul_self_gpow {G : Type w} [group G] (b : G) (m : ) :
b * b ^ m = b ^ (m + 1)

theorem mul_gpow_self {G : Type w} [group G] (b : G) (m : ) :
(b ^ m) * b = b ^ (m + 1)

theorem add_gsmul {A : Type y} [add_group A] (a : A) (i j : ) :
(i + j) •ℤ a = i •ℤ a + j •ℤ a

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

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

theorem gpow_one_add {G : Type w} [group G] (a : G) (i : ) :
a ^ (1 + i) = a * a ^ i

theorem one_add_gsmul {A : Type y} [add_group A] (a : A) (i : ) :
(1 + i) •ℤ a = a + i •ℤ a

theorem gpow_mul_comm {G : Type w} [group G] (a : G) (i j : ) :
(a ^ i) * a ^ j = (a ^ j) * a ^ i

theorem gsmul_add_comm {A : Type y} [add_group A] (a : A) (i j : ) :
i •ℤ a + j •ℤ a = j •ℤ a + i •ℤ a

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

theorem gsmul_mul' {A : Type y} [add_group A] (a : A) (m n : ) :
m * n •ℤ a = n •ℤ (m •ℤ a)

theorem gpow_mul' {G : Type w} [group G] (a : G) (m n : ) :
a ^ m * n = (a ^ n) ^ m

theorem gsmul_mul {A : Type y} [add_group A] (a : A) (m n : ) :
m * n •ℤ a = m •ℤ (n •ℤ a)

theorem gpow_bit0 {G : Type w} [group G] (a : G) (n : ) :
a ^ bit0 n = (a ^ n) * a ^ n

theorem bit0_gsmul {A : Type y} [add_group A] (a : A) (n : ) :
bit0 n •ℤ a = n •ℤ a + n •ℤ a

theorem gpow_bit1 {G : Type w} [group G] (a : G) (n : ) :
a ^ bit1 n = ((a ^ n) * a ^ n) * a

theorem bit1_gsmul {A : Type y} [add_group A] (a : A) (n : ) :
bit1 n •ℤ a = n •ℤ a + n •ℤ a + a

theorem monoid_hom.map_gpow {G : Type w} {H : Type x} [group G] [group H] (f : G →* H) (a : G) (n : ) :
f (a ^ n) = f a ^ n

theorem add_monoid_hom.map_gsmul {A : Type y} {B : Type z} [add_group A] [add_group B] (f : A →+ B) (a : A) (n : ) :
f (n •ℤ a) = n •ℤ f a

@[simp]
theorem units.coe_gpow {G : Type w} [group G] (u : units G) (n : ) :
(u ^ n) = u ^ n

Lemmas about gsmul under ordering, placed here (rather than in algebra.group_power.basic with their friends) because they require facts from data.int.basic

theorem gsmul_pos {A : Type y} {a : A} (ha : 0 < a) {k : } :
0 < k0 < k •ℤ a

theorem gsmul_le_gsmul {A : Type y} {a : A} {n m : } :
0 an mn •ℤ a m •ℤ a

theorem gsmul_lt_gsmul {A : Type y} {a : A} {n m : } :
0 < an < mn •ℤ a < m •ℤ a

theorem gsmul_le_gsmul_iff {A : Type y} {a : A} {n m : } :
0 < a(n •ℤ a m •ℤ a n m)

theorem gsmul_lt_gsmul_iff {A : Type y} {a : A} {n m : } :
0 < a(n •ℤ a < m •ℤ a n < m)

theorem nsmul_le_nsmul_iff {A : Type y} {a : A} {n m : } :
0 < a(n •ℕ a m •ℕ a n m)

theorem nsmul_lt_nsmul_iff {A : Type y} {a : A} {n m : } :
0 < a(n •ℕ a < m •ℕ a n < m)

@[simp]
theorem with_bot.coe_nsmul {A : Type y} [add_monoid A] (a : A) (n : ) :

theorem nsmul_eq_mul' {R : Type u₁} [semiring R] (a : R) (n : ) :
n •ℕ a = a * n

@[simp]
theorem nsmul_eq_mul {R : Type u₁} [semiring R] (n : ) (a : R) :
n •ℕ a = (n) * a

theorem mul_nsmul_left {R : Type u₁} [semiring R] (a b : R) (n : ) :
n •ℕ a * b = a * (n •ℕ b)

theorem mul_nsmul_assoc {R : Type u₁} [semiring R] (a b : R) (n : ) :
n •ℕ a * b = (n •ℕ a) * b

@[simp]
theorem nat.cast_pow {R : Type u₁} [semiring R] (n m : ) :
(n ^ m) = n ^ m

@[simp]
theorem int.coe_nat_pow (n m : ) :
(n ^ m) = n ^ m

theorem int.nat_abs_pow (n : ) (k : ) :
(n ^ k).nat_abs = n.nat_abs ^ k

theorem bit0_mul {R : Type u₁} [ring R] {n r : R} :
(bit0 n) * r = 2 •ℤ n * r

theorem mul_bit0 {R : Type u₁} [ring R] {n r : R} :
r * bit0 n = 2 •ℤ r * n

theorem bit1_mul {R : Type u₁} [ring R] {n r : R} :
(bit1 n) * r = 2 •ℤ n * r + r

theorem mul_bit1 {R : Type u₁} [ring R] {n r : R} :
r * bit1 n = 2 •ℤ r * n + r

@[simp]
theorem gsmul_eq_mul {R : Type u₁} [ring R] (a : R) (n : ) :
n •ℤ a = (n) * a

theorem gsmul_eq_mul' {R : Type u₁} [ring R] (a : R) (n : ) :
n •ℤ a = a * n

theorem mul_gsmul_left {R : Type u₁} [ring R] (a b : R) (n : ) :
n •ℤ a * b = a * (n •ℤ b)

theorem mul_gsmul_assoc {R : Type u₁} [ring R] (a b : R) (n : ) :
n •ℤ a * b = (n •ℤ a) * b

@[simp]
theorem gsmul_int_int (a b : ) :
a •ℤ b = a * b

theorem gsmul_int_one (n : ) :
n •ℤ 1 = n

@[simp]
theorem int.cast_pow {R : Type u₁} [ring R] (n : ) (m : ) :
(n ^ m) = n ^ m

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

theorem one_add_mul_le_pow' {R : Type u₁} {a : R} (Hsqr : 0 a * a) (H : 0 1 + a) (n : ) :
1 + n •ℕ a (1 + a) ^ n

Bernoulli's inequality. This version works for semirings but requires an additional hypothesis 0 ≤ a * a.

theorem pow_lt_pow_of_lt_one {R : Type u₁} {a : R} (h : 0 < a) (ha : a < 1) {i j : } :
i < ja ^ j < a ^ i

theorem pow_le_pow_of_le_one {R : Type u₁} {a : R} (h : 0 a) (ha : a 1) {i j : } :
i ja ^ j a ^ i

theorem pow_le_one {R : Type u₁} {x : R} (n : ) :
0 xx 1x ^ n 1

theorem one_add_mul_le_pow {R : Type u₁} {a : R} (H : -2 a) (n : ) :
1 + n •ℕ a (1 + a) ^ n

Bernoulli's inequality for n : ℕ, -2 ≤ a.

theorem one_add_sub_mul_le_pow {R : Type u₁} {a : R} (H : -1 a) (n : ) :
1 + n •ℕ (a - 1) a ^ n

Bernoulli's inequality reformulated to estimate a^n.

theorem int.units_pow_two (u : units ) :
u ^ 2 = 1

theorem int.units_pow_eq_pow_mod_two (u : units ) (n : ) :
u ^ n = u ^ (n % 2)

@[simp]
theorem int.nat_abs_pow_two (x : ) :
(x.nat_abs) ^ 2 = x ^ 2

def powers_hom (M : Type u) [monoid M] :
M

Monoid homomorphisms from multiplicative ℕ are defined by the image of multiplicative.of_add 1.

Equations
def gpowers_hom (G : Type w) [group G] :
G

Monoid homomorphisms from multiplicative ℤ are defined by the image of multiplicative.of_add 1.

Equations
def multiples_hom (A : Type y) [add_monoid A] :
A ( →+ A)

Additive homomorphisms from ℕ are defined by the image of 1.

Equations
def gmultiples_hom (A : Type y) [add_group A] :
A ( →+ A)

Additive homomorphisms from ℤ are defined by the image of 1.

Equations
@[simp]
theorem powers_hom_apply {M : Type u} [monoid M] (x : M) (n : multiplicative ) :
((powers_hom M) x) n =

@[simp]
theorem powers_hom_symm_apply {M : Type u} [monoid M] (f : →* M) :

@[simp]
theorem gpowers_hom_apply {G : Type w} [group G] (x : G) (n : multiplicative ) :
((gpowers_hom G) x) n =

@[simp]
theorem gpowers_hom_symm_apply {G : Type w} [group G] (f : →* G) :

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

@[simp]
theorem multiples_hom_symm_apply {A : Type y} [add_monoid A] (f : →+ A) :

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

@[simp]
theorem gmultiples_hom_symm_apply {A : Type y} [add_group A] (f : →+ A) :

theorem monoid_hom.apply_mnat {M : Type u} [monoid M] (f : →* M) (n : multiplicative ) :
f n =

theorem monoid_hom.ext_mnat {M : Type u} [monoid M] ⦃f g : →* M⦄ :
= f = g

theorem monoid_hom.apply_mint {M : Type u} [group M] (f : →* M) (n : multiplicative ) :
f n =

theorem monoid_hom.ext_mint {M : Type u} [group M] ⦃f g : →* M⦄ :
= f = g

theorem add_monoid_hom.apply_nat {M : Type u} [add_monoid M] (f : →+ M) (n : ) :
f n = n •ℕ f 1

add_monoid_hom.ext_nat is defined in data.nat.cast

theorem add_monoid_hom.apply_int {M : Type u} [add_group M] (f : →+ M) (n : ) :
f n = n •ℤ f 1

add_monoid_hom.ext_int is defined in data.int.cast

def powers_mul_hom (M : Type u) [comm_monoid M] :
M ≃*

If M is commutative, powers_hom is a multiplicative equivalence.

Equations
def gpowers_mul_hom (G : Type w) [comm_group G] :
G ≃*

If M is commutative, gpowers_hom is a multiplicative equivalence.

Equations
def multiples_add_hom (A : Type y)  :
A ≃+ ( →+ A)

If M is commutative, multiples_hom is an additive equivalence.

Equations
def gmultiples_add_hom (A : Type y)  :
A ≃+ ( →+ A)

If M is commutative, gmultiples_hom is an additive equivalence.

Equations
@[simp]
theorem powers_mul_hom_apply {M : Type u} [comm_monoid M] (x : M) (n : multiplicative ) :
( x) n =

@[simp]
theorem powers_mul_hom_symm_apply {M : Type u} [comm_monoid M] (f : →* M) :

@[simp]
theorem gpowers_mul_hom_apply {G : Type w} [comm_group G] (x : G) (n : multiplicative ) :
( x) n =

@[simp]
theorem gpowers_mul_hom_symm_apply {G : Type w} [comm_group G] (f : →* G) :

@[simp]
theorem multiples_add_hom_apply {A : Type y} (x : A) (n : ) :
( x) n = n •ℕ x

@[simp]
theorem multiples_add_hom_symm_apply {A : Type y} (f : →+ A) :
.symm) f = f 1

@[simp]
theorem gmultiples_add_hom_apply {A : Type y} (x : A) (n : ) :
( x) n = n •ℤ x

@[simp]
theorem gmultiples_add_hom_symm_apply {A : Type y} (f : →+ A) :
.symm) f = f 1

### Commutativity (again)

Facts about semiconj_by and commute that require gpow or gsmul, or the fact that integer multiplication equals semiring multiplication.

@[simp]
theorem semiconj_by.cast_nat_mul_right {R : Type u₁} [semiring R] {a x y : R} (h : x y) (n : ) :
((n) * x) ((n) * y)

@[simp]
theorem semiconj_by.cast_nat_mul_left {R : Type u₁} [semiring R] {a x y : R} (h : x y) (n : ) :
semiconj_by ((n) * a) x y

@[simp]
theorem semiconj_by.cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a x y : R} (h : x y) (m n : ) :
semiconj_by ((m) * a) ((n) * x) ((n) * y)

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

@[simp]
theorem semiconj_by.cast_int_mul_right {R : Type u₁} [ring R] {a x y : R} (h : x y) (m : ) :
((m) * x) ((m) * y)

@[simp]
theorem semiconj_by.cast_int_mul_left {R : Type u₁} [ring R] {a x y : R} (h : x y) (m : ) :
semiconj_by ((m) * a) x y

@[simp]
theorem semiconj_by.cast_int_mul_cast_int_mul {R : Type u₁} [ring R] {a x y : R} (h : x y) (m n : ) :
semiconj_by ((m) * a) ((n) * x) ((n) * y)

@[simp]
theorem commute.cast_nat_mul_right {R : Type u₁} [semiring R] {a b : R} (h : b) (n : ) :
((n) * b)

@[simp]
theorem commute.cast_nat_mul_left {R : Type u₁} [semiring R] {a b : R} (h : b) (n : ) :
commute ((n) * a) b

@[simp]
theorem commute.cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a b : R} (h : b) (m n : ) :
commute ((m) * a) ((n) * b)

@[simp]
theorem commute.self_cast_nat_mul {R : Type u₁} [semiring R] {a : R} (n : ) :
((n) * a)

@[simp]
theorem commute.cast_nat_mul_self {R : Type u₁} [semiring R] {a : R} (n : ) :
commute ((n) * a) a

@[simp]
theorem commute.self_cast_nat_mul_cast_nat_mul {R : Type u₁} [semiring R] {a : R} (m n : ) :
commute ((m) * a) ((n) * a)

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

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

@[simp]
theorem commute.cast_int_mul_right {R : Type u₁} [ring R] {a b : R} (h : b) (m : ) :
((m) * b)

@[simp]
theorem commute.cast_int_mul_left {R : Type u₁} [ring R] {a b : R} (h : b) (m : ) :
commute ((m) * a) b

theorem commute.cast_int_mul_cast_int_mul {R : Type u₁} [ring R] {a b : R} (h : b) (m n : ) :
commute ((m) * a) ((n) * b)

@[simp]
theorem commute.self_cast_int_mul {R : Type u₁} [ring R] (a : R) (n : ) :
((n) * a)

@[simp]
theorem commute.cast_int_mul_self {R : Type u₁} [ring R] (a : R) (n : ) :
commute ((n) * a) a

theorem commute.self_cast_int_mul_cast_int_mul {R : Type u₁} [ring R] (a : R) (m n : ) :
commute ((m) * a) ((n) * a)

@[simp]

@[simp]
theorem nat.of_add_mul (a b : ) :

@[simp]

@[simp]

@[simp]
theorem int.of_add_mul (a b : ) :

theorem units.conj_pow {M : Type u} [monoid M] (u : units M) (x : M) (n : ) :
(((u) * x) * u⁻¹) ^ n = ((u) * x ^ n) * u⁻¹

theorem units.conj_pow' {M : Type u} [monoid M] (u : units M) (x : M) (n : ) :
(((u⁻¹) * x) * u) ^ n = ((u⁻¹) * x ^ n) * u

@[simp]
theorem units.op_pow {M : Type u} [monoid M] (x : M) (n : ) :
opposite.op (x ^ n) = ^ n

Moving to the opposite monoid commutes with taking powers.

@[simp]
theorem units.unop_pow {M : Type u} [monoid M] (x : Mᵒᵖ) (n : ) :