Content created by Egbert Rijke and Gregor Perčič.
Created on 2023-09-21.
Last modified on 2023-11-24.
open import elementary-number-theory.group-of-integers open import foundation.universe-levels open import group-theory.free-groups-with-one-generator open import group-theory.groups open import group-theory.intersections-subgroups-groups open import group-theory.kernels-homomorphisms-groups open import group-theory.subgroups
hom-element-Group G g : ℤ → G
Note that our conventions are slightly different from the conventions in
classical mathematics, where the exponent is taken to be the positive integer
generates the subgroup
ℤ that we call the exponent of
G. In constructive mathematics, however,
such an integer is not always well-defined.