# Elements of finite order

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-06.

module group-theory.elements-of-finite-order-groups where

Imports
open import elementary-number-theory.group-of-integers
open import elementary-number-theory.nonzero-integers

open import foundation.existential-quantification
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.orders-of-elements-groups
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-elements-groups


## Idea

An element x of a group G is said to be of finite order if the subgroup order x of ℤ is generated by a nonzero integer.

Note that the condition of being of finite order is slightly stronger than the condition of being a torsion element. The latter condition merely asserts that there exists a nonzero integer in the subgroup order x of ℤ.

## Definitions

### The predicate of being an element of finite order

module _
{l1 : Level} (G : Group l1) (x : type-Group G)
where

has-finite-order-element-prop-Group : Prop l1
has-finite-order-element-prop-Group =
∃ ( nonzero-ℤ)
( λ k →
has-same-elements-prop-Subgroup ℤ-Group
( subgroup-element-Group ℤ-Group (int-nonzero-ℤ k))
( subgroup-order-element-Group G x))