mathlib documentation

group_theory.order_of_element

Order of an element #

This file defines the order of an element of a finite group. For a finite group G the order of g ∈ G is the minimal n ≥ 1 such that g ^ n = 1.

Main definitions #

Tags #

order of an element

TODO #

source
def add_order_of {H : Type u} [add_monoid H] (x : H) :
ℕ

add_order_of h is the additive order of the element x, i.e. the n ≥ 1, s. t. n • x = 0 if it exists. Otherwise, i.e. if x is of infinite order, then add_order_of x is 0 by convention.

Equations
source
def order_of {α : Type u} [monoid α] (a : α) :
ℕ

order_of a is the order of the element a, i.e. the n ≥ 1, s.t. a ^ n = 1 if it exists. Otherwise, i.e. if a is of infinite order, then order_of a is 0 by convention.

Equations
source
@[simp]
theorem add_order_of_of_mul_eq_order_of {α : Type u} [monoid α] (a : α) :
add_order_of (⇑additive.of_mul a) = order_of a
source
@[simp]
theorem order_of_of_add_eq_add_order_of {H : Type u} [add_monoid H] (x : H) :
order_of (⇑multiplicative.of_add x) = add_order_of x
source
theorem add_order_of_pos' {H : Type u} [add_monoid H] {x : H} (h : ∃ (n : ℕ), 0 < n ∧ n • x = 0) :
0 < add_order_of x
source
theorem order_of_pos' {α : Type u} [monoid α] {a : α} (h : ∃ (n : ℕ), 0 < n ∧ a ^ n = 1) :
0 < order_of a
source
theorem pow_order_of_eq_one {α : Type u} [monoid α] (a : α) :
a ^ order_of a = 1
source
theorem add_order_of_nsmul_eq_zero {H : Type u} [add_monoid H] (x : H) :
add_order_of x • x = 0
source
theorem add_order_of_eq_zero {H : Type u} [add_monoid H] {a : H} (h : ∀ (n : ℕ), 0 < n → n • a ≠ 0) :
add_order_of a = 0
source
theorem order_of_eq_zero {α : Type u} [monoid α] {a : α} (h : ∀ (n : ℕ), 0 < n → a ^ n ≠ 1) :
order_of a = 0
source
theorem add_order_of_le_of_nsmul_eq_zero' {H : Type u} [add_monoid H] {x : H} {m : ℕ} (h : m < add_order_of x) :
¬(0 < m ∧ m • x = 0)
source
theorem order_of_le_of_pow_eq_one' {α : Type u} {a : α} [monoid α] {m : ℕ} (h : m < order_of a) :
¬(0 < m ∧ a ^ m = 1)
source
theorem add_order_of_le_of_nsmul_eq_zero {H : Type u} [add_monoid H] {x : H} {n : ℕ} (hn : 0 < n) (h : n • x = 0) :
add_order_of x ≤ n
source
theorem order_of_le_of_pow_eq_one {α : Type u} {a : α} [monoid α] {n : ℕ} (hn : 0 < n) (h : a ^ n = 1) :
order_of a ≤ n
source
@[simp]
theorem order_of_one {α : Type u} [monoid α] :
order_of 1 = 1
source
@[simp]
theorem add_order_of_zero {H : Type u} [add_monoid H] :
add_order_of 0 = 1
source
@[simp]
theorem order_of_eq_one_iff {α : Type u} {a : α} [monoid α] :
order_of a = 1 ↔ a = 1
source
@[simp]
theorem add_order_of_eq_one_iff {H : Type u} [add_monoid H] {x : H} :
add_order_of x = 1 ↔ x = 0
source
theorem pow_eq_mod_order_of {α : Type u} {a : α} [monoid α] {n : ℕ} :
a ^ n = a ^ (n % order_of a)
source
theorem nsmul_eq_mod_add_order_of {H : Type u} [add_monoid H] {x : H} {n : ℕ} :
n • x = (n % add_order_of x) • x
source
theorem order_of_dvd_of_pow_eq_one {α : Type u} {a : α} [monoid α] {n : ℕ} (h : a ^ n = 1) :
order_of a ∣ n
source
theorem add_order_of_dvd_of_nsmul_eq_zero {H : Type u} [add_monoid H] {x : H} {n : ℕ} (h : n • x = 0) :
add_order_of x ∣ n
source
theorem add_order_of_dvd_iff_nsmul_eq_zero {H : Type u} [add_monoid H] {x : H} {n : ℕ} :
add_order_of x ∣ n ↔ n • x = 0
source
theorem order_of_dvd_iff_pow_eq_one {α : Type u} {a : α} [monoid α] {n : ℕ} :
order_of a ∣ n ↔ a ^ n = 1
source
theorem commute.order_of_mul_dvd_lcm {α : Type u} {a b : α} [monoid α] (h : commute a b) :
order_of (a * b) ∣ (order_of a).lcm (order_of b)
source
theorem add_order_of_eq_prime {H : Type u} [add_monoid H] {x : H} {p : ℕ} [hp : fact (nat.prime p)] (hg : p • x = 0) (hg1 : x ≠ 0) :
add_order_of x = p
source
theorem order_of_eq_prime {α : Type u} {a : α} [monoid α] {p : ℕ} [hp : fact (nat.prime p)] (hg : a ^ p = 1) (hg1 : a ≠ 1) :
order_of a = p
source
theorem add_order_of_eq_add_order_of_iff {H : Type u} [add_monoid H] {x : H} {A : Type u_1} [add_monoid A] {y : A} :
add_order_of x = add_order_of y ↔ ∀ (n : ℕ), n • x = 0 ↔ n • y = 0
source
theorem order_of_eq_order_of_iff {α : Type u} {a : α} [monoid α] {β : Type u_1} [monoid β] {b : β} :
order_of a = order_of b ↔ ∀ (n : ℕ), a ^ n = 1 ↔ b ^ n = 1
source
theorem add_order_of_injective {A : Type u_1} {B : Type u_2} [add_monoid A] [add_monoid B] (f : A →+ B) (hf : function.injective ⇑f) (x : A) :
add_order_of (⇑f x) = add_order_of x
source
theorem order_of_injective {G : Type u_1} {H : Type u_2} [monoid G] [monoid H] (f : G →* H) (hf : function.injective ⇑f) (σ : G) :
order_of (⇑f σ) = order_of σ
source
@[simp]
theorem order_of_submonoid {G : Type u_1} [monoid G] {H : submonoid G} (σ : ↥H) :
order_of ↑σ = order_of σ
source
@[simp]
theorem order_of_add_submonoid {G : Type u_1} [add_monoid G] {H : add_submonoid G} (σ : ↥H) :
add_order_of ↑σ = add_order_of σ
source
@[simp]
theorem order_of_add_subgroup {G : Type u_1} [add_group G] {H : add_subgroup G} (σ : ↥H) :
add_order_of ↑σ = add_order_of σ
source
@[simp]
theorem order_of_subgroup {G : Type u_1} [group G] {H : subgroup G} (σ : ↥H) :
order_of ↑σ = order_of σ
source
theorem add_order_of_eq_prime_pow {H : Type u} [add_monoid H] {x : H} {p k : ℕ} (hprime : nat.prime p) (hnot : ¬p ^ k • x = 0) (hfin : p ^ (k + 1) • x = 0) :
add_order_of x = p ^ (k + 1)
source
theorem order_of_eq_prime_pow {α : Type u} {a : α} [monoid α] {p k : ℕ} (hprime : nat.prime p) (hnot : ¬a ^ p ^ k = 1) (hfin : a ^ p ^ (k + 1) = 1) :
order_of a = p ^ (k + 1)
source
theorem order_of_pow' {α : Type u} (a : α) [monoid α] {n : ℕ} (h : n ≠ 0) :
order_of (a ^ n) = order_of a / (order_of a).gcd n
source
theorem add_order_of_nsmul' {H : Type u} [add_monoid H] (x : H) {n : ℕ} (h : n ≠ 0) :
add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n
source
theorem order_of_pow'' {α : Type u} (a : α) [monoid α] (n : ℕ) (h : ∃ (n : ℕ), 0 < n ∧ a ^ n = 1) :
order_of (a ^ n) = order_of a / (order_of a).gcd n
source
theorem add_order_of_nsmul'' {H : Type u} [add_monoid H] (x : H) (n : ℕ) (h : ∃ (n : ℕ), 0 < n ∧ n • x = 0) :
add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n
source
theorem pow_injective_aux {α : Type u} (a : α) [left_cancel_monoid α] {n m : ℕ} (h : n ≤ m) (hm : m < order_of a) (eq : a ^ n = a ^ m) :
n = m
source
theorem nsmul_injective_aux {H : Type u} [add_left_cancel_monoid H] (x : H) {n m : ℕ} (h : n ≤ m) (hm : m < add_order_of x) (eq : n • x = m • x) :
n = m
source
theorem nsmul_injective_of_lt_add_order_of {H : Type u} [add_left_cancel_monoid H] (x : H) {n m : ℕ} (hn : n < add_order_of x) (hm : m < add_order_of x) (eq : n • x = m • x) :
n = m
source
theorem pow_injective_of_lt_order_of {α : Type u} (a : α) [left_cancel_monoid α] {n m : ℕ} (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) :
n = m
source
theorem gpow_eq_mod_order_of {α : Type u} {a : α} [group α] {i : ℤ} :
a ^ i = a ^ (i % ↑(order_of a))
source
theorem gsmul_eq_mod_add_order_of {H : Type u} [add_group H] {x : H} {i : ℤ} :
i •ℤ x = i % ↑(add_order_of x) •ℤ x
source
theorem sum_card_add_order_of_eq_card_nsmul_eq_zero {H : Type u} [fintype H] [add_monoid H] [decidable_eq H] {n : ℕ} (hn : 0 < n) :
∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), (finset.filter (λ (x : H), add_order_of x = m) finset.univ).card = (finset.filter (λ (x : H), n • x = 0) finset.univ).card
source
theorem sum_card_order_of_eq_card_pow_eq_one {α : Type u} [fintype α] [monoid α] [decidable_eq α] {n : ℕ} (hn : 0 < n) :
∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), (finset.filter (λ (a : α), order_of a = m) finset.univ).card = (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card
source
theorem exists_pow_eq_one {α : Type u} [fintype α] [left_cancel_monoid α] (a : α) :
∃ (i : ℕ), 0 < i ∧ a ^ i = 1

TODO: Use this to show that a finite left cancellative monoid is a group.

source
theorem exists_nsmul_eq_zero {H : Type u} [fintype H] [add_left_cancel_monoid H] (x : H) :
∃ (i : ℕ), 0 < i ∧ i • x = 0
source
theorem add_order_of_le_card_univ {H : Type u} [fintype H] [add_left_cancel_monoid H] {x : H} :
add_order_of x ≤ fintype.card H
source
theorem order_of_le_card_univ {α : Type u} [fintype α] [left_cancel_monoid α] {a : α} :
order_of a ≤ fintype.card α
source
theorem order_of_pos {α : Type u} [fintype α] [left_cancel_monoid α] (a : α) :
0 < order_of a

This is the same as `order_of_pos' but with one fewer explicit assumption since this is automatic in case of a finite cancellative monoid.

source
theorem add_order_of_pos {H : Type u} [fintype H] [add_left_cancel_monoid H] (x : H) :
0 < add_order_of x

This is the same as `add_order_of_pos' but with one fewer explicit assumption since this is automatic in case of a finite cancellative additive monoid.

source
theorem exists_pow_eq_self_of_coprime {n : ℕ} {α : Type u_1} [monoid α] {a : α} (h : n.coprime (order_of a)) :
∃ (m : ℕ), (a ^ n) ^ m = a
source
theorem exists_nsmul_eq_self_of_coprime {n : ℕ} {H : Type u_1} [add_monoid H] (x : H) (h : n.coprime (add_order_of x)) :
∃ (m : ℕ), m • n • x = x
source
theorem order_of_pow {α : Type u} [fintype α] [left_cancel_monoid α] {n : ℕ} (a : α) :
order_of (a ^ n) = order_of a / (order_of a).gcd n

This is the same as order_of_pow' and order_of_pow'' but with one assumption less which is automatic in the case of a finite cancellative monoid.

source
theorem add_order_of_nsmul {H : Type u} [fintype H] [add_left_cancel_monoid H] {n : ℕ} (x : H) :
add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n

This is the same as add_order_of_nsmul' and add_order_of_nsmul but with one assumption less which is automatic in the case of a finite cancellative additive monoid.

source
theorem mem_multiples_iff_mem_range_add_order_of {H : Type u} [fintype H] [add_left_cancel_monoid H] [decidable_eq H] {x x' : H} :
x' ∈ add_submonoid.multiples x ↔ x' ∈ finset.image (λ (_x : ℕ), _x • x) (finset.range (add_order_of x))
source
theorem mem_powers_iff_mem_range_order_of {α : Type u} [fintype α] [left_cancel_monoid α] [decidable_eq α] {a a' : α} :
a' ∈ submonoid.powers a ↔ a' ∈ finset.image (pow a) (finset.range (order_of a))
source
@[instance]
def decidable_multiples {H : Type u} [fintype H] [add_left_cancel_monoid H] [decidable_eq H] {x : H} :
decidable_pred ↑(add_submonoid.multiples x)
Equations
source
@[instance]
def decidable_powers {α : Type u} {a : α} [fintype α] [left_cancel_monoid α] [decidable_eq α] :
decidable_pred ↑(submonoid.powers a)
Equations
source
theorem order_eq_card_powers {α : Type u} [fintype α] [left_cancel_monoid α] [decidable_eq α] {a : α} :
order_of a = fintype.card ↥↑(submonoid.powers a)
source
theorem add_order_of_eq_card_multiples {H : Type u} [fintype H] [add_left_cancel_monoid H] [decidable_eq H] {x : H} :
add_order_of x = fintype.card ↥↑(add_submonoid.multiples x)
source
theorem exists_gpow_eq_one {α : Type u} [fintype α] [group α] (a : α) :
∃ (i : ℤ) (H : i ≠ 0), a ^ i = 1
source
theorem exists_gsmul_eq_zero {H : Type u} [fintype H] [add_group H] (x : H) :
∃ (i : ℤ) (H_1 : i ≠ 0), i •ℤ x = 0
source
theorem mem_multiples_iff_mem_gmultiples {H : Type u} [fintype H] [add_group H] {x y : H} :
y ∈ add_submonoid.multiples x ↔ y ∈ add_subgroup.gmultiples x
source
theorem mem_powers_iff_mem_gpowers {α : Type u} [fintype α] [group α] {a x : α} :
x ∈ submonoid.powers a ↔ x ∈ subgroup.gpowers a
source
theorem multiples_eq_gmultiples {H : Type u} [fintype H] [add_group H] (x : H) :
↑(add_submonoid.multiples x) = ↑(add_subgroup.gmultiples x)
source
theorem powers_eq_gpowers {α : Type u} [fintype α] [group α] (a : α) :
↑(submonoid.powers a) = ↑(subgroup.gpowers a)
source
theorem mem_gmultiples_iff_mem_range_add_order_of {H : Type u} [fintype H] [add_group H] [decidable_eq H] {x x' : H} :
x' ∈ add_subgroup.gmultiples x ↔ x' ∈ finset.image (λ (_x : ℕ), _x • x) (finset.range (add_order_of x))
source
theorem mem_gpowers_iff_mem_range_order_of {α : Type u} [fintype α] [group α] [decidable_eq α] {a a' : α} :
a' ∈ subgroup.gpowers a ↔ a' ∈ finset.image (pow a) (finset.range (order_of a))
source
@[instance]
def decidable_gmultiples {H : Type u} [fintype H] [add_group H] [decidable_eq H] {x : H} :
decidable_pred ↑(add_subgroup.gmultiples x)
Equations
source
@[instance]
def decidable_gpowers {α : Type u} {a : α} [fintype α] [group α] [decidable_eq α] :
decidable_pred ↑(subgroup.gpowers a)
Equations
source
theorem order_eq_card_gpowers {α : Type u} [fintype α] [group α] [decidable_eq α] {a : α} :
order_of a = fintype.card ↥↑(subgroup.gpowers a)
source
theorem add_order_eq_card_gmultiples {H : Type u} [fintype H] [add_group H] [decidable_eq H] {x : H} :
add_order_of x = fintype.card ↥↑(add_subgroup.gmultiples x)
source
theorem order_of_dvd_card_univ {α : Type u} {a : α} [fintype α] [group α] :
order_of a ∣ fintype.card α
source
theorem add_order_of_dvd_card_univ {H : Type u} [fintype H] [add_group H] {x : H} :
add_order_of x ∣ fintype.card H
source
@[simp]
theorem pow_card_eq_one {α : Type u} [fintype α] [group α] {a : α} :
a ^ fintype.card α = 1
source
@[simp]
theorem card_nsmul_eq_zero {H : Type u} [fintype H] [add_group H] {x : H} :
fintype.card H • x = 0
source
theorem image_range_add_order_of {H : Type u} [fintype H] [add_group H] [decidable_eq H] {x : H} :
finset.image (λ (i : ℕ), i • x) (finset.range (add_order_of x)) = ↑(add_subgroup.gmultiples x).to_finset
source
theorem image_range_order_of {α : Type u} (a : α) [fintype α] [group α] [decidable_eq α] :
finset.image (λ (i : ℕ), a ^ i) (finset.range (order_of a)) = ↑(subgroup.gpowers a).to_finset

TODO: Generalise to submonoid.powers.

source
theorem gcd_nsmul_card_eq_zero_iff {H : Type u} [fintype H] [add_group H] {x : H} {n : ℕ} :
n • x = 0 ↔ n.gcd (fintype.card H) • x = 0
source
theorem pow_gcd_card_eq_one_iff {α : Type u} (a : α) [fintype α] [group α] {n : ℕ} :
a ^ n = 1 ↔ a ^ n.gcd (fintype.card α) = 1

TODO: Generalise to finite_cancel_monoid.