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 #
order_of
defines the order of an elementa
of a groupG
, by convention its value is0
ifa
has infinite order.
Tags #
order of an element
TODO #
- Move the first declarations until the definition of order to other files.
- Yury's suggestion: Redefine
order_of x := minimal_period (* x) 1
, this should maketo_additive
easier.
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.
TODO: Use this to show that a finite left cancellative monoid is a group.
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 = id (λ (x' : H), decidable_of_iff' (x' ∈ finset.image (λ (_x : ℕ), _x • x) (finset.range (add_order_of x))) _)
Equations
- decidable_powers = id (λ (a' : α), decidable_of_iff' (a' ∈ finset.image (pow a) (finset.range (order_of a))) _)
Equations
- decidable_gmultiples = decidable_gmultiples._proof_1.mpr decidable_multiples
Equations
- decidable_gpowers = decidable_gpowers._proof_1.mpr decidable_powers
TODO: Generalise to submonoid.powers
.