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 #
is_of_fin_orderis a predicate on an elementxof a monoidGsaying thatxis of finite order.is_of_fin_add_orderis the additive analogue ofis_of_fin_order.order_of xdefines the order of an elementxof a monoidG, by convention its value is0ifxhas infinite order.add_order_ofis the additive analogue oforder_of.
Tags #
order of an element
theorem
is_periodic_pt_add_iff_nsmul_eq_zero
{G : Type u}
{n : ℕ}
[add_monoid G]
(x : G) :
function.is_periodic_pt (has_add.add x) n 0 ↔ n • x = 0
theorem
is_periodic_pt_mul_iff_pow_eq_one
{G : Type u}
{n : ℕ}
[monoid G]
(x : G) :
function.is_periodic_pt (has_mul.mul x) n 1 ↔ x ^ n = 1
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
- is_of_fin_add_order a = (0 ∈ function.periodic_pts (has_add.add a))
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
- is_of_fin_order x = (1 ∈ function.periodic_pts (has_mul.mul x))
Elements of finite order are of finite order in submonoids.
Elements of finite order are of finite order in submonoids.
theorem
add_monoid_hom.is_of_fin_order
{G : Type u}
[add_monoid G]
{H : Type v}
[add_monoid H]
(f : G →+ H)
{x : G}
(h : is_of_fin_add_order x) :
is_of_fin_add_order (⇑f x)
The image of an element of finite additive order has finite additive order.
theorem
monoid_hom.is_of_fin_order
{G : Type u}
[monoid G]
{H : Type v}
[monoid H]
(f : G →* H)
{x : G}
(h : is_of_fin_order x) :
is_of_fin_order (⇑f x)
The image of an element of finite order has finite order.
theorem
is_of_fin_order.apply
{η : Type u_1}
{Gs : η → Type u_2}
[Π (i : η), monoid (Gs i)]
{x : Π (i : η), Gs i}
(h : is_of_fin_order x)
(i : η) :
is_of_fin_order (x i)
If a direct product has finite order then so does each component.
theorem
is_of_fin_add_order.apply
{η : Type u_1}
{Gs : η → Type u_2}
[Π (i : η), add_monoid (Gs i)]
{x : Π (i : η), Gs i}
(h : is_of_fin_add_order x)
(i : η) :
is_of_fin_add_order (x i)
If a direct product has finite additive order then so does each component.
0 is of finite order in any additive monoid.
1 is of finite order in any monoid.
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
- order_of x = function.minimal_period (has_mul.mul x) 1
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]
@[simp]
theorem
add_order_of_pos'
{G : Type u}
{x : G}
[add_monoid G]
(h : is_of_fin_add_order x) :
0 < add_order_of x
theorem
add_order_of_eq_zero
{G : Type u}
{x : G}
[add_monoid G]
(h : ¬is_of_fin_add_order x) :
add_order_of x = 0
theorem
add_order_of_eq_zero_iff
{G : Type u}
{x : G}
[add_monoid G] :
add_order_of x = 0 ↔ ¬is_of_fin_add_order x
theorem
add_order_of_pos_iff
{G : Type u}
{x : G}
[add_monoid G] :
0 < add_order_of x ↔ is_of_fin_add_order x
A group element has finite additive order iff its order is positive.
A group element has finite order iff its order is positive.
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) :
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) :
add_order_of x ≤ n
@[simp]
theorem
add_monoid.order_of_eq_one_iff
{G : Type u}
{x : G}
[add_monoid G] :
add_order_of x = 1 ↔ x = 0
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
add_order_of_dvd_of_nsmul_eq_zero
{G : Type u}
{x : G}
{n : ℕ}
[add_monoid G]
(h : n • x = 0) :
add_order_of x ∣ n
theorem
add_order_of_dvd_iff_nsmul_eq_zero
{G : Type u}
{x : G}
[add_monoid G]
{n : ℕ} :
add_order_of x ∣ n ↔ n • x = 0
theorem
add_order_of_map_dvd
{G : Type u}
[add_monoid G]
{H : Type u_1}
[add_monoid H]
(ψ : G →+ H)
(x : G) :
add_order_of (⇑ψ x) ∣ add_order_of x
theorem
exists_nsmul_eq_self_of_coprime
{G : Type u}
{x : G}
{n : ℕ}
[add_monoid G]
(h : n.coprime (add_order_of x)) :
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} :
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) :
add_order_of (⇑f x) = add_order_of x
@[simp, norm_cast]
theorem
add_order_of_nsmul'
{G : Type u}
(x : G)
{n : ℕ}
[add_monoid G]
(h : n ≠ 0) :
add_order_of (n • x) = add_order_of x / (add_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) :
add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n
theorem
add_order_of_nsmul_coprime
{G : Type u}
{y : G}
{m : ℕ}
[add_monoid G]
(h : (add_order_of y).coprime m) :
add_order_of (m • y) = add_order_of y
theorem
add_commute.order_of_add_dvd_lcm
{G : Type u}
[add_monoid G]
{x y : G}
(h : add_commute x y) :
add_order_of (x + y) ∣ (add_order_of x).lcm (add_order_of y)
theorem
add_commute.add_order_of_add_dvd_mul_add_order_of
{G : Type u}
[add_monoid G]
{x y : G}
(h : add_commute x y) :
add_order_of (x + y) ∣ add_order_of x * add_order_of y
theorem
add_commute.add_order_of_add_eq_mul_add_order_of_of_coprime
{G : Type u}
[add_monoid G]
{x y : G}
(h : add_commute x y)
(hco : (add_order_of x).coprime (add_order_of y)) :
add_order_of (x + y) = add_order_of x * add_order_of y
theorem
add_commute.is_of_fin_order_add
{G : Type u}
{y : G}
[add_monoid G]
{x : G}
(h : add_commute x y)
(hx : is_of_fin_add_order x)
(hy : is_of_fin_add_order y) :
is_of_fin_add_order (x + y)
Commuting elements of finite additive order are closed under addition.
theorem
commute.is_of_fin_order_mul
{G : Type u}
{y : G}
[monoid G]
{x : G}
(h : commute x y)
(hx : is_of_fin_order x)
(hy : is_of_fin_order y) :
is_of_fin_order (x * y)
Commuting elements of finite order are closed under multiplication.
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) :
add_order_of x = p
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
mem_powers_iff_mem_range_order_of'
{G : Type u}
(x y : G)
[left_cancel_monoid G]
[decidable_eq G]
(hx : 0 < order_of x) :
y ∈ submonoid.powers x ↔ y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))
theorem
mem_multiples_iff_mem_range_add_order_of'
{G : Type u}
(x y : G)
[add_left_cancel_monoid G]
[decidable_eq G]
(hx : 0 < add_order_of x) :
y ∈ add_submonoid.multiples x ↔ y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))
Inverses of elements of finite order have finite order.
Inverses of elements of finite additive order have finite additive order.
@[simp]
Inverses of elements of finite order have finite order.
@[simp]
Inverses of elements of finite additive order have finite additive order.
@[simp]
@[simp, norm_cast]
theorem
nsmul_inj_mod
{G : Type u}
{x : G}
[add_group G]
{n m : ℕ} :
n • x = m • x ↔ n % add_order_of x = m % add_order_of x
@[simp]
theorem
is_of_fin_add_order.zsmul
{G : Type u}
{x : G}
[add_group G]
(h : is_of_fin_add_order x)
{i : ℤ} :
is_of_fin_add_order (i • x)
theorem
is_of_fin_order.zpow
{G : Type u}
{x : G}
[group G]
(h : is_of_fin_order x)
{i : ℤ} :
is_of_fin_order (x ^ i)
theorem
is_of_fin_order.of_mem_zpowers
{G : Type u}
{x y : G}
[group G]
(h : is_of_fin_order x)
(h' : y ∈ subgroup.zpowers x) :
theorem
is_of_fin_add_order.of_mem_zmultiples
{G : Type u}
{x y : G}
[add_group G]
(h : is_of_fin_add_order x)
(h' : y ∈ add_subgroup.zmultiples x) :
theorem
add_order_of_dvd_of_mem_zmultiples
{G : Type u}
{x y : G}
[add_group G]
(h : y ∈ add_subgroup.zmultiples x) :
theorem
smul_eq_self_of_mem_zpowers
{G : Type u}
{x y : G}
[group G]
{α : Type u_1}
[mul_action G α]
(hx : x ∈ subgroup.zpowers y)
{a : α}
(hs : y • a = a) :
theorem
vadd_eq_self_of_mem_zmultiples
{α : Type u_1}
{G : Type u_2}
[add_group G]
[add_action G α]
{x y : G}
(hx : x ∈ add_subgroup.zmultiples y)
{a : α}
(hs : y +ᵥ a = a) :
theorem
is_of_fin_order.mul
{G : Type u}
{x y : G}
[comm_monoid G]
(hx : is_of_fin_order x)
(hy : is_of_fin_order y) :
is_of_fin_order (x * y)
Elements of finite order are closed under multiplication.
theorem
is_of_fin_add_order.add
{G : Type u}
{x y : G}
[add_comm_monoid G]
(hx : is_of_fin_add_order x)
(hy : is_of_fin_add_order y) :
is_of_fin_add_order (x + y)
Elements of finite additive order are closed under addition.
theorem
sum_card_order_of_eq_card_pow_eq_one
{G : Type u}
{n : ℕ}
[monoid G]
[fintype G]
[decidable_eq G]
(hn : 0 < n) :
(finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ)).sum (λ (m : ℕ), (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 : ℕ}
[add_monoid G]
[fintype G]
[decidable_eq G]
(hn : 0 < n) :
(finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ)).sum (λ (m : ℕ), (finset.filter (λ (x : G), add_order_of x = m) finset.univ).card) = (finset.filter (λ (x : G), n • x = 0) finset.univ).card
theorem
order_of_le_card_univ
{G : Type u}
{x : G}
[left_cancel_monoid G]
[fintype G] :
order_of x ≤ fintype.card 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}
[add_left_cancel_monoid G]
[finite G]
(x : G) :
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.
theorem
add_order_of_nsmul
{G : Type u}
{n : ℕ}
[add_left_cancel_monoid G]
[finite G]
(x : G) :
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.
theorem
mem_multiples_iff_mem_range_add_order_of
{G : Type u}
{x y : G}
[add_left_cancel_monoid G]
[finite G]
[decidable_eq G] :
y ∈ add_submonoid.multiples x ↔ y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))
theorem
mem_powers_iff_mem_range_order_of
{G : Type u}
{x y : G}
[left_cancel_monoid G]
[finite G]
[decidable_eq G] :
y ∈ submonoid.powers x ↔ y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))
@[protected, instance]
noncomputable
def
decidable_multiples
{G : Type u}
{x : G}
[add_left_cancel_monoid G] :
decidable_pred (λ (_x : G), _x ∈ add_submonoid.multiples x)
Equations
- decidable_multiples = classical.dec_pred (λ (_x : G), _x ∈ add_submonoid.multiples x)
@[protected, instance]
noncomputable
def
decidable_powers
{G : Type u}
{x : G}
[left_cancel_monoid G] :
decidable_pred (λ (_x : G), _x ∈ submonoid.powers x)
Equations
- decidable_powers = classical.dec_pred (λ (_x : G), _x ∈ submonoid.powers x)
noncomputable
def
fin_equiv_multiples
{G : Type u}
[add_left_cancel_monoid G]
[finite G]
(x : G) :
fin (add_order_of x) ≃ ↥↑(add_submonoid.multiples x)
The equivalence between fin (add_order_of a) and
add_submonoid.multiples a, sending i to i • a.
Equations
- fin_equiv_multiples x = equiv.of_bijective (λ (n : fin (add_order_of x)), ⟨↑n • x, _⟩) _
The equivalence between fin (order_of x) and submonoid.powers x, sending i to x ^ i."
Equations
- fin_equiv_powers x = equiv.of_bijective (λ (n : fin (order_of x)), ⟨x ^ ↑n, _⟩) _
@[simp]
theorem
fin_equiv_multiples_apply
{G : Type u}
[add_left_cancel_monoid G]
[finite G]
{x : G}
{n : fin (add_order_of x)} :
@[simp]
theorem
fin_equiv_powers_apply
{G : Type u}
[left_cancel_monoid G]
[finite G]
{x : G}
{n : fin (order_of x)} :
noncomputable
def
powers_equiv_powers
{G : Type u}
{x y : G}
[left_cancel_monoid G]
[finite G]
(h : order_of x = order_of y) :
↥↑(submonoid.powers x) ≃ ↥↑(submonoid.powers y)
The equivalence between submonoid.powers of two elements x, y of the same order, mapping
x ^ i to y ^ i.
Equations
- powers_equiv_powers h = (fin_equiv_powers x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_powers y))
noncomputable
def
multiples_equiv_multiples
{G : Type u}
{x y : G}
[add_left_cancel_monoid G]
[finite G]
(h : add_order_of x = add_order_of y) :
The equivalence between submonoid.multiples of two elements a, b of the same additive order,
mapping i • a to i • b.
Equations
- multiples_equiv_multiples h = (fin_equiv_multiples x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_multiples y))
@[simp]
theorem
multiples_equiv_multiples_apply
{G : Type u}
{x y : G}
[add_left_cancel_monoid G]
[finite G]
(h : add_order_of x = add_order_of y)
(n : ℕ) :
theorem
add_order_of_eq_card_multiples
{G : Type u}
{x : G}
[add_left_cancel_monoid G]
[fintype G] :
theorem
mem_powers_iff_mem_zpowers
{G : Type u}
{x y : G}
[group G]
[finite G] :
y ∈ submonoid.powers x ↔ y ∈ subgroup.zpowers x
theorem
powers_eq_zpowers
{G : Type u}
[group G]
[finite G]
(x : G) :
↑(submonoid.powers x) = ↑(subgroup.zpowers x)
theorem
mem_zmultiples_iff_mem_range_add_order_of
{G : Type u}
{x y : G}
[add_group G]
[finite G]
[decidable_eq G] :
y ∈ add_subgroup.zmultiples x ↔ y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))
theorem
mem_zpowers_iff_mem_range_order_of
{G : Type u}
{x y : G}
[group G]
[finite G]
[decidable_eq G] :
y ∈ subgroup.zpowers x ↔ y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))
@[protected, instance]
noncomputable
def
decidable_zmultiples
{G : Type u}
{x : G}
[add_group G] :
decidable_pred (λ (_x : G), _x ∈ add_subgroup.zmultiples x)
Equations
- decidable_zmultiples = classical.dec_pred (λ (_x : G), _x ∈ add_subgroup.zmultiples x)
@[protected, instance]
noncomputable
def
decidable_zpowers
{G : Type u}
{x : G}
[group G] :
decidable_pred (λ (_x : G), _x ∈ subgroup.zpowers x)
Equations
- decidable_zpowers = classical.dec_pred (λ (_x : G), _x ∈ subgroup.zpowers x)
The equivalence between fin (order_of x) and subgroup.zpowers x, sending i to x ^ i.
Equations
- fin_equiv_zpowers x = (fin_equiv_powers x).trans (equiv.set.of_eq _)
noncomputable
def
fin_equiv_zmultiples
{G : Type u}
[add_group G]
[finite G]
(x : G) :
fin (add_order_of x) ≃ ↥↑(add_subgroup.zmultiples x)
The equivalence between fin (add_order_of a) and subgroup.zmultiples a, sending i
to i • a.
Equations
@[simp]
theorem
fin_equiv_zmultiples_apply
{G : Type u}
{x : G}
[add_group G]
[finite G]
{n : fin (add_order_of x)} :
noncomputable
def
zmultiples_equiv_zmultiples
{G : Type u}
{x y : G}
[add_group G]
[finite G]
(h : add_order_of x = add_order_of y) :
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}
[group G]
[finite G]
(h : order_of x = order_of y) :
↥↑(subgroup.zpowers x) ≃ ↥↑(subgroup.zpowers y)
The equivalence between subgroup.zpowers of two elements x, y of the same order, mapping
x ^ i to y ^ i.
Equations
- zpowers_equiv_zpowers h = (fin_equiv_zpowers x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_zpowers y))
@[simp]
theorem
zmultiples_equiv_zmultiples_apply
{G : Type u}
{x y : G}
[add_group G]
[finite G]
(h : add_order_of x = add_order_of y)
(n : ℕ) :
See also add_order_eq_card_zmultiples'.
See also order_eq_card_zpowers'.
theorem
order_of_dvd_card_univ
{G : Type u}
{x : G}
[group G]
[fintype G] :
order_of x ∣ fintype.card G
theorem
add_order_of_dvd_nat_card
{G : Type u_1}
[add_group G]
{x : G} :
add_order_of x ∣ nat.card G
@[simp]
@[simp]
theorem
add_subgroup.nsmul_index_mem
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[H.normal]
(g : G) :
@[simp]
theorem
pow_coprime_one
{n : ℕ}
{G : Type u_1}
[group G]
(h : (nat.card G).coprime n) :
⇑(pow_coprime h) 1 = 1
@[simp]
theorem
nsmul_coprime_zero
{n : ℕ}
{G : Type u_1}
[add_group G]
(h : (nat.card G).coprime n) :
⇑(nsmul_coprime h) 0 = 0
@[simp]
theorem
pow_coprime_inv
{n : ℕ}
{G : Type u_1}
[group G]
(h : (nat.card G).coprime n)
{g : G} :
⇑(pow_coprime h) g⁻¹ = (⇑(pow_coprime h) g)⁻¹
@[simp]
theorem
nsmul_coprime_neg
{n : ℕ}
{G : Type u_1}
[add_group G]
(h : (nat.card G).coprime n)
{g : G} :
⇑(nsmul_coprime h) (-g) = -⇑(nsmul_coprime h) g
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)) :
theorem
image_range_add_order_of
{G : Type u}
{x : G}
[add_group G]
[fintype G]
[decidable_eq G] :
finset.image (λ (i : ℕ), i • x) (finset.range (add_order_of x)) = ↑(add_subgroup.zmultiples x).to_finset
@[nolint]
theorem
image_range_order_of
{G : Type u}
{x : G}
[group G]
[fintype G]
[decidable_eq G] :
finset.image (λ (i : ℕ), x ^ i) (finset.range (order_of x)) = ↑(subgroup.zpowers x).to_finset
TODO: Generalise to submonoid.powers.
TODO: Generalise to finite + cancel_monoid.
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
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
@[simp]
theorem
smul_card_add_subgroup_coe
{G : Type u_1}
[add_group G]
[fintype G]
(S : set G)
(hS : S.nonempty) :
↑(smul_card_add_subgroup S hS) = fintype.card G • S
If S is a nonempty subset of a finite add group G,
then |G| • S is a subgroup
Equations
- smul_card_add_subgroup S hS = have one_mem : 0 ∈ fintype.card G • S, from _, add_subgroup_of_idempotent (fintype.card G • S) _ _
@[simp]
theorem
pow_card_subgroup_coe
{G : Type u_1}
[group G]
[fintype G]
(S : set G)
(hS : S.nonempty) :
↑(pow_card_subgroup S hS) = S ^ fintype.card G
def
pow_card_subgroup
{G : Type u_1}
[group G]
[fintype G]
(S : set G)
(hS : S.nonempty) :
subgroup G
If S is a nonempty subset of a finite group G, then S ^ |G| is a subgroup
Equations
- pow_card_subgroup S hS = have one_mem : 1 ∈ S ^ fintype.card G, from _, subgroup_of_idempotent (S ^ fintype.card G) _ _