Finitely Generated Abelian Groups

Joseph Thommes and Manuel Eberl 🌐

July 7, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This article deals with the formalisation of some group-theoretic results including the fundamental theorem of finitely generated abelian groups characterising the structure of these groups as a uniquely determined product of cyclic groups. Both the invariant factor decomposition and the primary decomposition are covered. Additional work includes results about the direct product, the internal direct product and more group-theoretic lemmas.

License

BSD License

Topics

Session Finitely_Generated_Abelian_Groups

Used by

Cite

× 
@article{Finitely_Generated_Abelian_Groups-AFP,
  author  = {Joseph Thommes and Manuel Eberl},
  title   = {Finitely Generated Abelian Groups},
  journal = {Archive of Formal Proofs},
  month   = {July},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Finitely_Generated_Abelian_Groups.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: