mathlib documentation

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.

(Additive) monoid

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

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

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

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

source
theorem is_unit_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ℕ) (hx : x ^ n = 1) (hn : 0 < n) :
is_unit x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
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

source
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

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

source
@[simp]
theorem with_bot.coe_nsmul {A : Type y} [add_monoid A] (a : A) (n : ℕ) :
↑(n •ℕ a) = n •ℕ ↑a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
theorem one_add_mul_le_pow' {R : Type u₁} [linear_ordered_semiring R] {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.

source
theorem pow_lt_pow_of_lt_one {R : Type u₁} [linear_ordered_semiring R] {a : R} (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) :
a ^ j < a ^ i

source
theorem pow_le_pow_of_le_one {R : Type u₁} [linear_ordered_semiring R] {a : R} (h : 0 ≤ a) (ha : a ≤ 1) {i j : ℕ} (hij : i ≤ j) :
a ^ j ≤ a ^ i

source
theorem pow_le_one {R : Type u₁} [linear_ordered_semiring R] {x : R} (n : ℕ) (h0 : 0 ≤ x) (h1 : x ≤ 1) :
x ^ n ≤ 1

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

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

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

Bernoulli's inequality reformulated to estimate a^n.

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

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

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

source
def powers_hom (M : Type u) [monoid M] :
M ≃ (multiplicative ℕ →* M)

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

Equations
source
def gpowers_hom (G : Type w) [group G] :
G ≃ (multiplicative ℤ →* G)

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

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

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

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

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

Equations
source
@[simp]
theorem powers_hom_apply {M : Type u} [monoid M] (x : M) (n : multiplicative ℕ) :
⇑(⇑(powers_hom M) x) n = x ^ n.to_add

source
@[simp]
theorem powers_hom_symm_apply {M : Type u} [monoid M] (f : multiplicative ℕ →* M) :
⇑((powers_hom M).symm) f = ⇑f (multiplicative.of_add 1)

source
theorem mnat_monoid_hom_eq {M : Type u} [monoid M] (f : multiplicative ℕ →* M) (n : multiplicative ℕ) :
⇑f n = ⇑f (multiplicative.of_add 1) ^ n.to_add

source
theorem mnat_monoid_hom_ext {M : Type u} [monoid M] ⦃f g : multiplicative ℕ →* M⦄ (h : ⇑f (multiplicative.of_add 1) = ⇑g (multiplicative.of_add 1)) :
f = g

Commutativity (again)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
@[simp]
theorem nat.to_add_pow (a : multiplicative ℕ) (b : ℕ) :
(a ^ b).to_add = (a.to_add) * b

source
@[simp]
theorem nat.of_add_mul (a b : ℕ) :
multiplicative.of_add (a * b) = multiplicative.of_add a ^ b

source
@[simp]
theorem int.to_add_pow (a : multiplicative ℤ) (b : ℕ) :
(a ^ b).to_add = (a.to_add) * ↑b

source
@[simp]
theorem int.to_add_gpow (a : multiplicative ℤ) (b : ℤ) :
(a ^ b).to_add = (a.to_add) * b

source
@[simp]
theorem int.of_add_mul (a b : ℤ) :
multiplicative.of_add (a * b) = multiplicative.of_add a ^ b

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

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

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

Moving to the opposite monoid commutes with taking powers.

source
@[simp]
theorem units.unop_pow {M : Type u} [monoid M] (x : Mᵒᵖ) (n : ℕ) :
opposite.unop (x ^ n) = opposite.unop x ^ n