Exponent of a group #
This file defines the exponent of a group, or more generally a monoid. For a group G
it is defined
to be the minimal n≥1
such that g ^ n = 1
for all g ∈ G
. For a finite group G
,
it is equal to the lowest common multiple of the order of all elements of the group G
.
Main definitions #
Monoid.ExponentExists
is a predicate on a monoidG
saying that there is some positiven
such thatg ^ n = 1
for allg ∈ G
.Monoid.exponent
defines the exponent of a monoidG
as the minimal positiven
such thatg ^ n = 1
for allg ∈ G
, by convention it is0
if no suchn
exists.AddMonoid.ExponentExists
the additive version ofMonoid.ExponentExists
.AddMonoid.exponent
the additive version ofMonoid.exponent
.
Main results #
Monoid.lcm_order_eq_exponent
: For a finite left cancel monoidG
, the exponent is equal to theFinset.lcm
of the order of its elements.Monoid.exponent_eq_iSup_orderOf(')
: For a commutative cancel monoid, the exponent is equal to⨆ g : G, orderOf g
(or zero if it has any order-zero elements).
TODO #
- Refactor the characteristic of a ring to be the exponent of its underlying additive group.
A predicate on an additive monoid saying that there is a positive integer n
such
that n • g = 0
for all g
.
Instances For
A predicate on a monoid saying that there is a positive integer n
such that g ^ n = 1
for all g
.
Instances For
The exponent of an additive group is the smallest positive integer n
such that
n • g = 0
for all g ∈ G
if it exists, otherwise it is zero by convention.
Instances For
The exponent of a group is the smallest positive integer n
such that g ^ n = 1
for all
g ∈ G
if it exists, otherwise it is zero by convention.