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 x ∈ G is the minimal n ≥ 1 such that x ^ n = 1.

Main definitions #

Tags #

order of an element

theorem is_periodic_pt_add_iff_nsmul_eq_zero {G : Type u} {n : } [add_monoid G] (x : G) :
theorem is_periodic_pt_mul_iff_pow_eq_one {G : Type u} {n : } [monoid G] (x : G) :
def is_of_fin_add_order {A : Type v} [add_monoid A] (a : A) :
Prop

is_of_fin_add_order is a predicate on an element a of an additive monoid to be of finite order, i.e. there exists n ≥ 1 such that n • a = 0.

Equations
def is_of_fin_order {G : Type u} [monoid G] (x : G) :
Prop

is_of_fin_order is a predicate on an element x of a monoid to be of finite order, i.e. there exists n ≥ 1 such that x ^ n = 1.

Equations
theorem is_of_fin_order_iff_pow_eq_one {G : Type u} [monoid G] (x : G) :
is_of_fin_order x ∃ (n : ), 0 < n x ^ n = 1
theorem is_of_fin_add_order_iff_nsmul_eq_zero {G : Type u} [add_monoid G] (x : G) :
is_of_fin_add_order x ∃ (n : ), 0 < n n x = 0
noncomputable def order_of {G : Type u} [monoid G] (x : G) :

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

Equations
noncomputable def add_order_of {G : Type u} [add_monoid G] (x : G) :

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

Equations
@[simp]
theorem add_order_of_pos' {G : Type u} {x : G} [add_monoid G] (h : is_of_fin_add_order x) :
theorem order_of_pos' {G : Type u} {x : G} [monoid G] (h : is_of_fin_order x) :
theorem pow_order_of_eq_one {G : Type u} [monoid G] (x : G) :
x ^ order_of x = 1
theorem add_order_of_nsmul_eq_zero {G : Type u} [add_monoid G] (x : G) :
theorem order_of_eq_zero {G : Type u} {x : G} [monoid G] (h : ¬is_of_fin_order x) :
theorem add_order_of_eq_zero {G : Type u} {x : G} [add_monoid G] (h : ¬is_of_fin_add_order x) :
theorem order_of_eq_zero_iff {G : Type u} {x : G} [monoid G] :
theorem order_of_eq_zero_iff' {G : Type u} {x : G} [monoid G] :
order_of x = 0 ∀ (n : ), 0 < nx ^ n 1
theorem add_order_of_eq_zero_iff' {G : Type u} {x : G} [add_monoid G] :
add_order_of x = 0 ∀ (n : ), 0 < nn x 0
theorem pow_ne_one_of_lt_order_of' {G : Type u} {x : G} {n : } [monoid G] (n0 : n 0) (h : n < order_of x) :
x ^ n 1
theorem nsmul_ne_zero_of_lt_add_order_of' {G : Type u} {x : G} {n : } [add_monoid G] (n0 : n 0) (h : n < add_order_of x) :
n x 0
theorem add_order_of_le_of_nsmul_eq_zero {G : Type u} {x : G} {n : } [add_monoid G] (hn : 0 < n) (h : n x = 0) :
theorem order_of_le_of_pow_eq_one {G : Type u} {x : G} {n : } [monoid G] (hn : 0 < n) (h : x ^ n = 1) :
@[simp]
theorem order_of_one {G : Type u} [monoid G] :
@[simp]
theorem order_of_zero {G : Type u} [add_monoid G] :
@[simp]
theorem order_of_eq_one_iff {G : Type u} {x : G} [monoid G] :
order_of x = 1 x = 1
@[simp]
theorem add_monoid.order_of_eq_one_iff {G : Type u} {x : G} [add_monoid G] :
theorem pow_eq_mod_order_of {G : Type u} {x : G} [monoid G] {n : } :
x ^ n = x ^ (n % order_of x)
theorem nsmul_eq_mod_add_order_of {G : Type u} {x : G} [add_monoid G] {n : } :
n x = (n % add_order_of x) x
theorem order_of_dvd_of_pow_eq_one {G : Type u} {x : G} {n : } [monoid G] (h : x ^ n = 1) :
theorem add_order_of_dvd_of_nsmul_eq_zero {G : Type u} {x : G} {n : } [add_monoid G] (h : n x = 0) :
theorem add_order_of_dvd_iff_nsmul_eq_zero {G : Type u} {x : G} [add_monoid G] {n : } :
theorem order_of_dvd_iff_pow_eq_one {G : Type u} {x : G} [monoid G] {n : } :
order_of x n x ^ n = 1
theorem exists_pow_eq_self_of_coprime {G : Type u} {x : G} {n : } [monoid G] (h : n.coprime (order_of x)) :
∃ (m : ), (x ^ n) ^ m = x
theorem exists_nsmul_eq_self_of_coprime {G : Type u} {x : G} {n : } [add_monoid G] (h : n.coprime (add_order_of x)) :
∃ (m : ), m n x = x
theorem add_order_of_eq_of_nsmul_and_div_prime_nsmul {G : Type u} {x : G} {n : } [add_monoid G] (hn : 0 < n) (hx : n x = 0) (hd : ∀ (p : ), nat.prime pp n(n / p) x 0) :
theorem order_of_eq_of_pow_and_pow_div_prime {G : Type u} {x : G} {n : } [monoid G] (hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ (p : ), nat.prime pp nx ^ (n / p) 1) :

If x^n = 1, but x^(n/p) ≠ 1 for all prime factors p of r, then x has order n in G.

theorem order_of_eq_order_of_iff {G : Type u} {x : G} [monoid G] {H : Type u_1} [monoid H] {y : H} :
order_of x = order_of y ∀ (n : ), x ^ n = 1 y ^ n = 1
theorem add_order_of_eq_add_order_of_iff {G : Type u} {x : G} [add_monoid G] {H : Type u_1} [add_monoid H] {y : H} :
add_order_of x = add_order_of y ∀ (n : ), n x = 0 n y = 0
theorem order_of_injective {G : Type u} [monoid G] {H : Type u_1} [monoid H] (f : G →* H) (hf : function.injective f) (x : G) :
theorem add_order_of_injective {G : Type u} [add_monoid G] {H : Type u_1} [add_monoid H] (f : G →+ H) (hf : function.injective f) (x : G) :
@[simp, norm_cast]
theorem order_of_submonoid {G : Type u} [monoid G] {H : submonoid G} (y : H) :
@[simp, norm_cast]
theorem order_of_add_submonoid {G : Type u} [add_monoid G] {H : add_submonoid G} (y : H) :
theorem order_of_units {G : Type u} [monoid G] {y : Gˣ} :
theorem order_of_add_units {G : Type u} [add_monoid G] {y : add_units G} :
theorem add_order_of_nsmul' {G : Type u} (x : G) {n : } [add_monoid G] (h : n 0) :
theorem order_of_pow' {G : Type u} (x : G) {n : } [monoid G] (h : n 0) :
order_of (x ^ n) = order_of x / (order_of x).gcd n
theorem add_order_of_nsmul'' {G : Type u} (x : G) (n : ) [add_monoid G] (h : is_of_fin_add_order x) :
theorem order_of_pow'' {G : Type u} (x : G) (n : ) [monoid G] (h : is_of_fin_order x) :
order_of (x ^ n) = order_of x / (order_of x).gcd n
theorem commute.order_of_mul_dvd_lcm {G : Type u} [monoid G] {x y : G} (h : commute x y) :
theorem add_commute.order_of_add_dvd_lcm {G : Type u} [add_monoid G] {x y : G} (h : add_commute x y) :
theorem commute.order_of_mul_dvd_mul_order_of {G : Type u} [monoid G] {x y : G} (h : commute x y) :
theorem commute.order_of_mul_eq_mul_order_of_of_coprime {G : Type u} [monoid G] {x y : G} (h : commute x y) (hco : (order_of x).coprime (order_of y)) :
theorem add_order_of_eq_prime {G : Type u} {x : G} [add_monoid G] {p : } [hp : fact (nat.prime p)] (hg : p x = 0) (hg1 : x 0) :
theorem order_of_eq_prime {G : Type u} {x : G} [monoid G] {p : } [hp : fact (nat.prime p)] (hg : x ^ p = 1) (hg1 : x 1) :
theorem add_order_of_eq_prime_pow {G : Type u} {x : G} {n : } [add_monoid G] {p : } [hp : fact (nat.prime p)] (hnot : ¬p ^ n x = 0) (hfin : p ^ (n + 1) x = 0) :
add_order_of x = p ^ (n + 1)
theorem order_of_eq_prime_pow {G : Type u} {x : G} {n : } [monoid G] {p : } [hp : fact (nat.prime p)] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :
order_of x = p ^ (n + 1)
theorem nsmul_injective_aux {G : Type u} (x : G) {n m : } [add_left_cancel_monoid G] (h : n m) (hm : m < add_order_of x) (eq : n x = m x) :
n = m
theorem pow_injective_aux {G : Type u} (x : G) {n m : } [left_cancel_monoid G] (h : n m) (hm : m < order_of x) (eq : x ^ n = x ^ m) :
n = m
theorem nsmul_injective_of_lt_add_order_of {G : Type u} (x : G) {n m : } [add_left_cancel_monoid G] (hn : n < add_order_of x) (hm : m < add_order_of x) (eq : n x = m x) :
n = m
theorem pow_injective_of_lt_order_of {G : Type u} (x : G) {n m : } [left_cancel_monoid G] (hn : n < order_of x) (hm : m < order_of x) (eq : x ^ n = x ^ m) :
n = m
theorem order_of_dvd_iff_zpow_eq_one {G : Type u} {x : G} [group G] {i : } :
(order_of x) i x ^ i = 1
theorem add_order_of_dvd_iff_zsmul_eq_zero {G : Type u} {x : G} [add_group G] {i : } :
@[simp, norm_cast]
theorem order_of_add_subgroup {G : Type u} [add_group G] {H : add_subgroup G} (y : H) :
@[simp, norm_cast]
theorem order_of_subgroup {G : Type u} [group G] {H : subgroup G} (y : H) :
theorem zsmul_eq_mod_add_order_of {G : Type u} {x : G} [add_group G] {i : } :
i x = (i % (add_order_of x)) x
theorem zpow_eq_mod_order_of {G : Type u} {x : G} [group G] {i : } :
x ^ i = x ^ (i % (order_of x))
theorem pow_inj_iff_of_order_of_eq_zero {G : Type u} {x : G} [group G] (h : order_of x = 0) {n m : } :
x ^ n = x ^ m n = m
theorem nsmul_inj_iff_of_add_order_of_eq_zero {G : Type u} {x : G} [add_group G] (h : add_order_of x = 0) {n m : } :
n x = m x n = m
theorem nsmul_inj_mod {G : Type u} {x : G} [add_group G] {n m : } :
theorem pow_inj_mod {G : Type u} {x : G} [group G] {n m : } :
x ^ n = x ^ m n % order_of x = m % order_of x
theorem sum_card_order_of_eq_card_pow_eq_one {G : Type u} {n : } [fintype G] [monoid G] [decidable_eq G] (hn : 0 < n) :
∑ (m : ) in finset.filter (λ (_x : ), _x n) (finset.range n.succ), (finset.filter (λ (x : G), order_of x = m) finset.univ).card = (finset.filter (λ (x : G), x ^ n = 1) finset.univ).card
theorem sum_card_add_order_of_eq_card_nsmul_eq_zero {G : Type u} {n : } [fintype G] [add_monoid G] [decidable_eq G] (hn : 0 < n) :
∑ (m : ) in finset.filter (λ (_x : ), _x n) (finset.range n.succ), (finset.filter (λ (x : G), add_order_of x = m) finset.univ).card = (finset.filter (λ (x : G), n x = 0) finset.univ).card
theorem exists_pow_eq_one {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :
theorem order_of_le_card_univ {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] :
theorem order_of_pos {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :

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.

theorem add_order_of_pos {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) :

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.

theorem add_order_of_nsmul {G : Type u} {n : } [fintype G] [add_left_cancel_monoid G] (x : G) :

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.

theorem order_of_pow {G : Type u} {n : } [fintype G] [left_cancel_monoid G] (x : G) :
order_of (x ^ n) = order_of x / (order_of x).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.

@[protected, instance]
noncomputable def decidable_multiples {G : Type u} {x : G} [fintype G] [add_left_cancel_monoid G] [decidable_eq G] :
Equations
@[protected, instance]
noncomputable def decidable_powers {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :
decidable_pred (λ (_x : G), _x submonoid.powers x)
Equations
noncomputable def fin_equiv_multiples {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) :

The equivalence between fin (add_order_of a) and add_submonoid.multiples a, sending i to i • a.

Equations
noncomputable def fin_equiv_powers {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :

The equivalence between fin (order_of x) and submonoid.powers x, sending i to x ^ i."

Equations
@[simp]
theorem fin_equiv_multiples_apply {G : Type u} [fintype G] [add_left_cancel_monoid G] {x : G} {n : fin (add_order_of x)} :
@[simp]
theorem fin_equiv_powers_apply {G : Type u} [fintype G] [left_cancel_monoid G] {x : G} {n : fin (order_of x)} :
(fin_equiv_powers x) n = x ^ n, _⟩
@[simp]
theorem fin_equiv_multiples_symm_apply {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) (n : ) {hn : ∃ (m : ), m x = n x} :
@[simp]
theorem fin_equiv_powers_symm_apply {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) (n : ) {hn : ∃ (m : ), x ^ m = x ^ n} :
((fin_equiv_powers x).symm) x ^ n, hn⟩ = n % order_of x, _⟩
noncomputable def powers_equiv_powers {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] (h : order_of x = order_of y) :

The equivalence between submonoid.powers of two elements x, y of the same order, mapping x ^ i to y ^ i.

Equations

The equivalence between submonoid.multiples of two elements a, b of the same additive order, mapping i • a to i • b.

Equations
@[simp]
theorem powers_equiv_powers_apply {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] (h : order_of x = order_of y) (n : ) :
(powers_equiv_powers h) x ^ n, _⟩ = y ^ n, _⟩
@[simp]
theorem multiples_equiv_multiples_apply {G : Type u} {x y : G} [fintype G] [add_left_cancel_monoid G] (h : add_order_of x = add_order_of y) (n : ) :
theorem exists_zpow_eq_one {G : Type u} [fintype G] [group G] (x : G) :
∃ (i : ) (H : i 0), x ^ i = 1
theorem exists_zsmul_eq_zero {G : Type u} [fintype G] [add_group G] (x : G) :
∃ (i : ) (H : i 0), i x = 0
theorem mem_powers_iff_mem_zpowers {G : Type u} {x y : G} [fintype G] [group G] :
theorem powers_eq_zpowers {G : Type u} [fintype G] [group G] (x : G) :
@[protected, instance]
noncomputable def decidable_zmultiples {G : Type u} {x : G} [fintype G] [add_group G] [decidable_eq G] :
Equations
@[protected, instance]
noncomputable def decidable_zpowers {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :
decidable_pred (λ (_x : G), _x subgroup.zpowers x)
Equations
noncomputable def fin_equiv_zpowers {G : Type u} [fintype G] [group G] (x : G) :

The equivalence between fin (order_of x) and subgroup.zpowers x, sending i to x ^ i.

Equations
noncomputable def fin_equiv_zmultiples {G : Type u} [fintype G] [add_group G] (x : G) :

The equivalence between fin (add_order_of a) and subgroup.zmultiples a, sending i to i • a.

Equations
@[simp]
theorem fin_equiv_zpowers_apply {G : Type u} {x : G} [fintype G] [group G] {n : fin (order_of x)} :
@[simp]
theorem fin_equiv_zmultiples_apply {G : Type u} {x : G} [fintype G] [add_group G] {n : fin (add_order_of x)} :
@[simp]
theorem fin_equiv_zmultiples_symm_apply {G : Type u} [fintype G] [add_group G] (x : G) (n : ) {hn : ∃ (m : ), m x = n x} :
@[simp]
theorem fin_equiv_zpowers_symm_apply {G : Type u} [fintype G] [group G] (x : G) (n : ) {hn : ∃ (m : ), x ^ m = x ^ n} :
((fin_equiv_zpowers x).symm) x ^ n, hn⟩ = n % order_of x, _⟩

The equivalence between subgroup.zmultiples of two elements a, b of the same additive order, mapping i • a to i • b.

Equations
noncomputable def zpowers_equiv_zpowers {G : Type u} {x y : G} [fintype G] [group G] (h : order_of x = order_of y) :

The equivalence between subgroup.zpowers of two elements x, y of the same order, mapping x ^ i to y ^ i.

Equations
@[simp]
theorem zmultiples_equiv_zmultiples_apply {G : Type u} {x y : G} [fintype G] [add_group G] (h : add_order_of x = add_order_of y) (n : ) :
@[simp]
theorem zpowers_equiv_zpowers_apply {G : Type u} {x y : G} [fintype G] [group G] (h : order_of x = order_of y) (n : ) :
(zpowers_equiv_zpowers h) x ^ n, _⟩ = y ^ n, _⟩
theorem order_of_dvd_card_univ {G : Type u} {x : G} [fintype G] [group G] :
theorem add_order_of_dvd_card_univ {G : Type u} {x : G} [fintype G] [add_group G] :
@[simp]
theorem pow_card_eq_one {G : Type u} {x : G} [fintype G] [group G] :
@[simp]
theorem card_nsmul_eq_zero {G : Type u} {x : G} [fintype G] [add_group G] :
theorem nsmul_eq_mod_card {G : Type u} {x : G} [fintype G] [add_group G] (n : ) :
n x = (n % fintype.card G) x
theorem pow_eq_mod_card {G : Type u} {x : G} [fintype G] [group G] (n : ) :
x ^ n = x ^ (n % fintype.card G)
theorem zpow_eq_mod_card {G : Type u} {x : G} [fintype G] [group G] (n : ) :
x ^ n = x ^ (n % (fintype.card G))
theorem zsmul_eq_mod_card {G : Type u} {x : G} [fintype G] [add_group G] (n : ) :
n x = (n % (fintype.card G)) x
@[simp]
theorem pow_coprime_symm_apply {G : Type u} {n : } [fintype G] [group G] (h : (fintype.card G).coprime n) (g : G) :
def pow_coprime {G : Type u} {n : } [fintype G] [group G] (h : (fintype.card G).coprime n) :
G G

If gcd(|G|,n)=1 then the nth power map is a bijection

Equations
@[simp]
theorem pow_coprime_apply {G : Type u} {n : } [fintype G] [group G] (h : (fintype.card G).coprime n) (g : G) :
(pow_coprime h) g = g ^ n
@[simp]
theorem nsmul_coprime_symm_apply {G : Type u} {n : } [fintype G] [add_group G] (h : (fintype.card G).coprime n) (g : G) :
@[simp]
theorem nsmul_coprime_apply {G : Type u} {n : } [fintype G] [add_group G] (h : (fintype.card G).coprime n) (g : G) :
def nsmul_coprime {G : Type u} {n : } [fintype G] [add_group G] (h : (fintype.card G).coprime n) :
G G

If gcd(|G|,n)=1 then the smul by n is a bijection

Equations
@[simp]
theorem pow_coprime_zero {G : Type u} {n : } [fintype G] [add_group G] (h : (fintype.card G).coprime n) :
@[simp]
theorem pow_coprime_one {G : Type u} {n : } [fintype G] [group G] (h : (fintype.card G).coprime n) :
@[simp]
theorem pow_coprime_inv {G : Type u} {n : } [fintype G] [group G] (h : (fintype.card G).coprime n) {g : G} :
@[simp]
theorem pow_coprime_neg {G : Type u} {n : } [fintype G] [add_group G] (h : (fintype.card G).coprime n) {g : G} :
theorem inf_eq_bot_of_coprime {G : Type u_1} [group G] {H K : subgroup G} [fintype H] [fintype K] (h : (fintype.card H).coprime (fintype.card K)) :
H K =
theorem add_inf_eq_bot_of_coprime {G : Type u_1} [add_group G] {H K : add_subgroup G} [fintype H] [fintype K] (h : (fintype.card H).coprime (fintype.card K)) :
H K =
theorem image_range_order_of {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :

TODO: Generalise to submonoid.powers.

theorem pow_gcd_card_eq_one_iff {G : Type u} {x : G} {n : } [fintype G] [group G] :
x ^ n = 1 x ^ n.gcd (fintype.card G) = 1

TODO: Generalise to finite_cancel_monoid.

theorem gcd_nsmul_card_eq_zero_iff {G : Type u} {x : G} {n : } [fintype G] [add_group G] :
n x = 0 n.gcd (fintype.card G) x = 0
def add_submonoid_of_idempotent {M : Type u_1} [add_left_cancel_monoid M] [fintype M] (S : set M) (hS1 : S.nonempty) (hS2 : S + S = S) :

A nonempty idempotent subset of a finite cancellative add monoid is a submonoid

Equations
def submonoid_of_idempotent {M : Type u_1} [left_cancel_monoid M] [fintype M] (S : set M) (hS1 : S.nonempty) (hS2 : S * S = S) :

A nonempty idempotent subset of a finite cancellative monoid is a submonoid

Equations
def add_subgroup_of_idempotent {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS1 : S.nonempty) (hS2 : S + S = S) :

A nonempty idempotent subset of a finite add group is a subgroup

Equations
def subgroup_of_idempotent {G : Type u_1} [group G] [fintype G] (S : set G) (hS1 : S.nonempty) (hS2 : S * S = S) :

A nonempty idempotent subset of a finite group is a subgroup

Equations
@[simp]
theorem smul_card_add_subgroup_coe {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS : S.nonempty) :
def smul_card_add_subgroup {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS : S.nonempty) :

If S is a nonempty subset of a finite add group G, then |G| • S is a subgroup

Equations
@[simp]
theorem pow_card_subgroup_coe {G : Type u_1} [group G] [fintype G] (S : set G) (hS : S.nonempty) :
def pow_card_subgroup {G : Type u_1} [group G] [fintype G] (S : set G) (hS : S.nonempty) :

If S is a nonempty subset of a finite group G, then S ^ |G| is a subgroup

Equations
theorem order_of_abs_ne_one {G : Type u} {x : G} [linear_ordered_ring G] (h : |x| 1) :