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 #

@[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 : ) :
(list.repeat a n).prod = a ^ n
@[simp]
theorem list.sum_repeat {A : Type y} [add_monoid A] (a : A) (n : ) :
(list.repeat a n).sum = n a
@[simp]
theorem units.coe_pow {M : Type u} [monoid M] (u : units M) (n : ) :
(u ^ n) = u ^ n
@[instance]
def invertible_pow {M : Type u} [monoid M] (m : M) [invertible m] (n : ) :
Equations
theorem inv_of_pow {M : Type u} [monoid M] (m : M) [invertible m] (n : ) [invertible (m ^ n)] :
(m ^ n) = m ^ n
theorem is_unit.pow {M : Type u} [monoid M] {m : M} (n : ) :
is_unit mis_unit (m ^ n)
def invertible_of_pow_succ_eq_one {M : Type u} [monoid M] (x : M) (n : ) (hx : x ^ n.succ = 1) :

If x ^ n.succ = 1 then x has an inverse, x^n.

Equations
def invertible_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : 0 < n) :

If x ^ n = 1 then x has an inverse, x^(n - 1).

Equations
theorem is_unit_of_pow_eq_one {M : Type u} [monoid M] (x : M) (n : ) (hx : x ^ n = 1) (hn : 0 < 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
@[simp]
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
@[simp]
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} [ordered_add_comm_group A] {a : A} (ha : 0 < a) {k : } (hk : 0 < k) :
0 < k •ℤ a
theorem gsmul_le_gsmul {A : Type y} [ordered_add_comm_group A] {a : A} {n m : } (ha : 0 a) (h : n m) :
n •ℤ a m •ℤ a
theorem gsmul_lt_gsmul {A : Type y} [ordered_add_comm_group A] {a : A} {n m : } (ha : 0 < a) (h : n < m) :
n •ℤ a < m •ℤ a
theorem abs_nsmul {α : Type u_1} [linear_ordered_add_comm_group α] (n : ) (a : α) :
abs (n a) = n abs a
theorem abs_gsmul {α : Type u_1} [linear_ordered_add_comm_group α] (n : ) (a : α) :
abs (n •ℤ a) = abs n •ℤ abs a
theorem abs_add_eq_add_abs_le {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} (hle : a b) :
abs (a + b) = abs a + abs b 0 a 0 b a 0 b 0
theorem abs_add_eq_add_abs_iff {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
abs (a + b) = abs a + abs b 0 a 0 b a 0 b 0
theorem gsmul_le_gsmul_iff {A : Type y} [linear_ordered_add_comm_group A] {a : A} {n m : } (ha : 0 < a) :
n •ℤ a m •ℤ a n m
theorem gsmul_lt_gsmul_iff {A : Type y} [linear_ordered_add_comm_group A] {a : A} {n m : } (ha : 0 < a) :
n •ℤ a < m •ℤ a n < m
theorem nsmul_le_nsmul_iff {A : Type y} [linear_ordered_add_comm_group A] {a : A} {n m : } (ha : 0 < a) :
n a m a n m
theorem nsmul_lt_nsmul_iff {A : Type y} [linear_ordered_add_comm_group A] {a : A} {n m : } (ha : 0 < a) :
n a < m a n < m
@[simp]
theorem with_bot.coe_nsmul {A : Type y} [add_monoid A] (a : A) (n : ) :
(n a) = n a
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₁} [ordered_semiring R] {a : R} (Hsqr : 0 a * a) (Hsqr' : 0 (1 + a) * (1 + a)) (H : 0 2 + a) (n : ) :
1 + (n) * a (1 + a) ^ n

Bernoulli's inequality. This version works for semirings but requires additional hypotheses 0 ≤ a * a and 0 ≤ (1 + a) * (1 + a).

theorem pow_lt_pow_of_lt_one {R : Type u₁} [ordered_semiring R] {a : R} (h : 0 < a) (ha : a < 1) {i j : } (hij : i < j) :
a ^ j < a ^ i
theorem pow_lt_pow_iff_of_lt_one {R : Type u₁} [ordered_semiring R] {a : R} {n m : } (hpos : 0 < a) (h : a < 1) :
a ^ m < a ^ n n < m
theorem pow_le_pow_of_le_one {R : Type u₁} [ordered_semiring R] {a : R} (h : 0 a) (ha : a 1) {i j : } (hij : i j) :
a ^ j a ^ i
theorem pow_le_one {R : Type u₁} [ordered_semiring R] {x : R} (n : ) (h0 : 0 x) (h1 : x 1) :
x ^ n 1
theorem sign_cases_of_C_mul_pow_nonneg {R : Type u₁} [linear_ordered_semiring R] {C r : R} (h : ∀ (n : ), 0 C * r ^ n) :
C = 0 0 < C 0 r
@[simp]
theorem abs_pow {R : Type u₁} [linear_ordered_ring R] (a : R) (n : ) :
abs (a ^ n) = abs a ^ n
@[simp]
theorem pow_bit1_neg_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } :
a ^ bit1 n < 0 a < 0
@[simp]
theorem pow_bit1_nonneg_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } :
0 a ^ bit1 n 0 a
@[simp]
theorem pow_bit1_nonpos_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } :
a ^ bit1 n 0 a 0
@[simp]
theorem pow_bit1_pos_iff {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } :
0 < a ^ bit1 n 0 < a
theorem pow_even_nonneg {R : Type u₁} [linear_ordered_ring R] {n : } (a : R) (hn : even n) :
0 a ^ n
theorem pow_even_pos {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } (ha : a 0) (hn : even n) :
0 < a ^ n
theorem pow_odd_nonneg {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } (ha : 0 a) (hn : odd n) :
0 a ^ n
theorem pow_odd_pos {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } (ha : 0 < a) (hn : odd n) :
0 < a ^ n
theorem pow_odd_nonpos {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } (ha : a 0) (hn : odd n) :
a ^ n 0
theorem pow_odd_neg {R : Type u₁} [linear_ordered_ring R] {a : R} {n : } (ha : a < 0) (hn : odd n) :
a ^ n < 0
theorem pow_even_abs {R : Type u₁} [linear_ordered_ring R] (a : R) {p : } (hp : even p) :
abs a ^ p = a ^ p
@[simp]
theorem pow_bit0_abs {R : Type u₁} [linear_ordered_ring R] (a : R) (p : ) :
abs a ^ bit0 p = a ^ bit0 p
theorem strict_mono_pow_bit1 {R : Type u₁} [linear_ordered_ring R] (n : ) :
strict_mono (λ (a : R), a ^ bit1 n)
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.

theorem one_add_mul_sub_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.

theorem nat.cast_le_pow_sub_div_sub {K : Type u_1} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ) :
n (a ^ n - 1) / (a - 1)

Bernoulli's inequality reformulated to estimate (n : K).

theorem nat.cast_le_pow_div_sub {K : Type u_1} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ) :
n a ^ n / (a - 1)

For any a > 1 and a natural n we have n ≤ a ^ n / (a - 1). See also nat.cast_le_pow_sub_div_sub for a stronger inequality with a ^ n - 1 in the numerator.

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
theorem int.abs_le_self_pow_two (a : ) :
(a.nat_abs) a ^ 2
theorem int.le_self_pow_two (b : ) :
b b ^ 2
def powers_hom (M : Type u) [monoid M] :

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

Equations
def gpowers_hom (G : Type w) [group 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 ) :
@[simp]
@[simp]
theorem gpowers_hom_apply {G : Type w} [group G] (x : G) (n : multiplicative ) :
@[simp]
@[simp]
theorem multiples_hom_apply {A : Type y} [add_monoid A] (x : A) (n : ) :
((multiples_hom A) 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 : ) :
@[simp]
theorem gmultiples_hom_symm_apply {A : Type y} [add_group A] (f : →+ A) :
@[ext]
theorem monoid_hom.ext_mnat {M : Type u} [monoid M] ⦃f g : multiplicative →* M⦄ (h : f (multiplicative.of_add 1) = g (multiplicative.of_add 1)) :
f = g

monoid_hom.ext_mint is defined in data.int.cast

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

If M is commutative, powers_hom is a multiplicative equivalence.

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

If M is commutative, gpowers_hom is a multiplicative equivalence.

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

If M is commutative, multiples_hom is an additive equivalence.

Equations
def gmultiples_add_hom (A : Type y) [add_comm_group A] :
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 ) :
@[simp]
theorem gpowers_mul_hom_apply {G : Type w} [comm_group G] (x : G) (n : multiplicative ) :
@[simp]
theorem multiples_add_hom_apply {A : Type y} [add_comm_monoid A] (x : A) (n : ) :
@[simp]
theorem multiples_add_hom_symm_apply {A : Type y} [add_comm_monoid A] (f : →+ A) :
@[simp]
theorem gmultiples_add_hom_apply {A : Type y} [add_comm_group A] (x : A) (n : ) :
@[simp]
theorem gmultiples_add_hom_symm_apply {A : Type y} [add_comm_group A] (f : →+ A) :

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 : semiconj_by a x y) (n : ) :
semiconj_by a ((n) * x) ((n) * y)
@[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
@[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)
@[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)
@[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)
@[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
@[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)
@[simp]
theorem commute.cast_nat_mul_right {R : Type u₁} [semiring R] {a b : R} (h : commute a b) (n : ) :
commute a ((n) * b)
@[simp]
theorem commute.cast_nat_mul_left {R : Type u₁} [semiring R] {a b : R} (h : commute a b) (n : ) :
commute ((n) * a) b
@[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)
@[simp]
theorem commute.self_cast_nat_mul {R : Type u₁} [semiring R] {a : R} (n : ) :
commute a ((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 : commute a u) (m : ) :
commute a (u ^ m)
@[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
@[simp]
theorem commute.cast_int_mul_right {R : Type u₁} [ring R] {a b : R} (h : commute a b) (m : ) :
commute a ((m) * b)
@[simp]
theorem commute.cast_int_mul_left {R : Type u₁} [ring R] {a b : R} (h : commute a b) (m : ) :
commute ((m) * a) b
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)
@[simp]
theorem commute.self_cast_int_mul {R : Type u₁} [ring R] (a : R) (n : ) :
commute a ((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)
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 : ) :

Moving to the opposite monoid commutes with taking powers.

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