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_ofdefines the order of an element
aof a group
G, by convention its value is
ahas infinite order.
order of an element
- 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 make
This is the same as
add_order_of_nsmul but with one assumption less
which is automatic in the case of a finite cancellative additive monoid.