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 #
IsOfFinOrder
is a predicate on an elementx
of a monoidG
saying thatx
is of finite order.IsOfFinAddOrder
is the additive analogue ofIsOfFinOrder
.orderOf x
defines the order of an elementx
of a monoidG
, by convention its value is0
ifx
has infinite order.addOrderOf
is the additive analogue oforderOf
.
Tags #
order of an element
IsOfFinAddOrder
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
- IsOfFinAddOrder x = (0 ∈ Function.periodicPts fun (x_1 : G) => x + x_1)
Instances For
IsOfFinOrder
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
- IsOfFinOrder x = (1 ∈ Function.periodicPts fun (x_1 : G) => x * x_1)
Instances For
Alias of the forward direction of isOfFinOrder_iff_pow_eq_one
.
See also injective_nsmul_iff_not_isOfFinAddOrder
.
See also injective_pow_iff_not_isOfFinOrder
.
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 additive order then so does each component.
If a direct product has finite order then so does each component.
0 is of finite order in any additive monoid.
1 is of finite order in any monoid.
The additive submonoid generated by an element is an additive group if that element has finite order.
Equations
- hx.addGroupMultiples = And.casesOn ⋯ fun (hpos : 0 < ⋯.choose) (hx_1 : ⋯.choose • x = 0) => AddSubmonoid.addGroupMultiples hpos hx_1
Instances For
The submonoid generated by an element is a group if that element has finite order.
Equations
- hx.groupPowers = And.casesOn ⋯ fun (hpos : 0 < ⋯.choose) (hx_1 : x ^ ⋯.choose = 1) => Submonoid.groupPowers hpos hx_1
Instances For
addOrderOf 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 addOrderOf a
is 0
by convention.
Equations
- addOrderOf x = Function.minimalPeriod (fun (x_1 : G) => x + x_1) 0
Instances For
A group element has finite additive order iff its order is positive.
A group element has finite order iff its order is positive.
Alias of nsmul_ne_zero_of_lt_addOrderOf
.
Alias of IsOfFinAddOrder.multiples_eq_image_range_addOrderOf
.
An injective homomorphism of additive monoids preserves orders of elements.
An additive equivalence preserves orders of elements.
If the order of x
is finite, then x
is a unit with inverse x ^ (orderOf x - 1)
.
Instances For
Commuting elements of finite additive order are closed under addition.
Commuting elements of finite order are closed under multiplication.
If each prime factor of
addOrderOf x
has higher multiplicity in addOrderOf y
, and x
commutes with y
,
then x + y
has the same order as y
.
If each prime factor of orderOf x
has higher multiplicity in orderOf y
, and x
commutes
with y
, then x * y
has the same order as y
.
The equivalence between Fin (addOrderOf a)
and
AddSubmonoid.multiples a
, sending i
to i • a
.
Equations
- finEquivMultiples x hx = Equiv.ofBijective (fun (n : Fin (addOrderOf x)) => ⟨↑n • x, ⋯⟩) ⋯
Instances For
The equivalence between Fin (orderOf x)
and Submonoid.powers x
, sending i
to x ^ i
."
Equations
- finEquivPowers x hx = Equiv.ofBijective (fun (n : Fin (orderOf x)) => ⟨x ^ ↑n, ⋯⟩) ⋯
Instances For
See also addOrder_eq_card_multiples
.
See also orderOf_eq_card_powers
.
Inverses of elements of finite additive order have finite additive order.
Inverses of elements of finite order have finite order.
Alias of the forward direction of isOfFinOrder_inv_iff
.
Inverses of elements of finite order have finite order.
Alias of the reverse direction of isOfFinOrder_inv_iff
.
Inverses of elements of finite order have finite order.
The equivalence between Fin (addOrderOf a)
and
Subgroup.zmultiples a
, sending i
to i • a
.
Equations
- finEquivZMultiples x hx = (finEquivMultiples x hx).trans (Equiv.Set.ofEq ⋯)
Instances For
The equivalence between Fin (orderOf x)
and Subgroup.zpowers x
, sending i
to x ^ i
.
Equations
- finEquivZPowers x hx = (finEquivPowers x hx).trans (Equiv.Set.ofEq ⋯)
Instances For
Elements of finite additive order are closed under addition.
Elements of finite order are closed under multiplication.
This is the same as IsOfFinAddOrder.addOrderOf_pos
but with one fewer explicit
assumption since this is automatic in case of a finite cancellative additive monoid.
This is the same as IsOfFinOrder.orderOf_pos
but with one fewer explicit assumption since this
is automatic in case of a finite cancellative monoid.
This is the same as addOrderOf_nsmul'
and
addOrderOf_nsmul
but with one assumption less which is automatic in the case of a
finite cancellative additive monoid.
This is the same as orderOf_pow'
and orderOf_pow''
but with one assumption less which is
automatic in the case of a finite cancellative monoid.
The equivalence between Submonoid.multiples
of two elements a, b
of the same additive order,
mapping i • a
to i • b
.
Equations
- multiplesEquivMultiples h = (finEquivMultiples x ⋯).symm.trans ((finCongr h).trans (finEquivMultiples y ⋯))
Instances For
The equivalence between Submonoid.powers
of two elements x, y
of the same order, mapping
x ^ i
to y ^ i
.
Equations
- powersEquivPowers h = (finEquivPowers x ⋯).symm.trans ((finCongr h).trans (finEquivPowers y ⋯))
Instances For
The equivalence between Subgroup.zmultiples
of two elements a, b
of the same additive order,
mapping i • a
to i • b
.
Equations
- zmultiplesEquivZMultiples h = (finEquivZMultiples x ⋯).symm.trans ((finCongr h).trans (finEquivZMultiples y ⋯))
Instances For
The equivalence between Subgroup.zpowers
of two elements x, y
of the same order, mapping
x ^ i
to y ^ i
.
Equations
- zpowersEquivZPowers h = (finEquivZPowers x ⋯).symm.trans ((finCongr h).trans (finEquivZPowers y ⋯))
Instances For
See also Nat.card_subgroup
.
See also Nat.card_addSubgroupZPowers
.
If gcd(|G|,n)=1
then the smul by n
is a bijection
Equations
- nsmulCoprime h = { toFun := fun (g : G) => n • g, invFun := fun (g : G) => (Nat.card G).gcdB n • g, left_inv := ⋯, right_inv := ⋯ }
Instances For
If gcd(|G|,n)=1
then the n
th power map is a bijection
Equations
- powCoprime h = { toFun := fun (g : G) => g ^ n, invFun := fun (g : G) => g ^ (Nat.card G).gcdB n, left_inv := ⋯, right_inv := ⋯ }
Instances For
A nonempty idempotent subset of a finite cancellative add monoid is a submonoid
Equations
- addSubmonoidOfIdempotent S hS1 hS2 = { carrier := S, add_mem' := ⋯, zero_mem' := ⋯ }
Instances For
A nonempty idempotent subset of a finite cancellative monoid is a submonoid
Equations
- submonoidOfIdempotent S hS1 hS2 = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯ }
Instances For
A nonempty idempotent subset of a finite add group is a subgroup
Equations
- addSubgroupOfIdempotent S hS1 hS2 = { carrier := S, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
A nonempty idempotent subset of a finite group is a subgroup
Equations
- subgroupOfIdempotent S hS1 hS2 = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
If S
is a nonempty subset of a finite add group G
, then |G| • S
is a subgroup
Equations
- smulCardAddSubgroup S hS = addSubgroupOfIdempotent (Fintype.card G • S) ⋯ ⋯
Instances For
If S
is a nonempty subset of a finite group G
, then S ^ |G|
is a subgroup
Equations
- powCardSubgroup S hS = subgroupOfIdempotent (S ^ Fintype.card G) ⋯ ⋯
Instances For
Alias of Prod.addOrderOf
.
Alias of addOrderOf_fst_dvd_addOrderOf
.
Alias of addOrderOf_snd_dvd_addOrderOf
.