Elements of finite order

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-06.
Last modified on 2024-04-11.

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))

See also

Recent changes