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_order
is a predicate on an elementx
of a monoidG
saying thatx
is of finite order.is_of_fin_add_order
is the additive analogue ofis_of_fin_order
.order_of x
defines the order of an elementx
of a monoidG
, by convention its value is0
ifx
has infinite order.add_order_of
is the additive analogue oforder_of
.
Tags #
order of an element
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.
The image of an element of finite additive order has finite additive order.
The image of an element of finite order has finite order.
If a direct product has finite order then so does each component.
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
A group element has finite additive order iff its order is positive.
A group element has finite order iff its order is positive.
If n * x = 0
, but n/p * x ≠ 0
for
all prime factors p
of n
, then x
has order n
in G
.
Commuting elements of finite additive order are closed under addition.
Commuting elements of finite order are closed under multiplication.
Inverses of elements of finite order have finite order.
Inverses of elements of finite additive order have finite additive order.
Inverses of elements of finite order have finite order.
Inverses of elements of finite additive order have finite additive order.
Elements of finite order are closed under multiplication.
Elements of finite additive order are closed under addition.
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.
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.
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.
Equations
- decidable_multiples = classical.dec_pred (λ (_x : G), _x ∈ add_submonoid.multiples x)
Equations
- decidable_powers = classical.dec_pred (λ (_x : G), _x ∈ submonoid.powers 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, _⟩) _
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))
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))
Equations
- decidable_zmultiples = classical.dec_pred (λ (_x : G), _x ∈ add_subgroup.zmultiples 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 _)
The equivalence between fin (add_order_of a)
and subgroup.zmultiples a
, sending i
to i • a
.
Equations
The equivalence between subgroup.zmultiples
of two elements a, b
of the same additive order,
mapping i • a
to i • b
.
Equations
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))
See also add_order_eq_card_zmultiples'
.
See also order_eq_card_zpowers'
.
If gcd(|G|,n)=1
then the n
th power map is a bijection
If gcd(|G|,n)=1
then the smul by n
is a bijection
TODO: Generalise to submonoid.powers
.
TODO: Generalise to finite
+ cancel_monoid
.
A nonempty idempotent subset of a finite cancellative add monoid is a submonoid
A nonempty idempotent subset of a finite cancellative monoid is a submonoid
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) _ _
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) _ _