Formalisation of Selected Results from Group Theory

Chair for Logic and Verification

Bachelor Thesis

This thesis deals with the formalisation of some group-theoretic results in Isabelle/HOL – an interactive theorem prover that machine-checks every proof step.

The results include the long-known and well understood fundamental theorem of finitely generated abelian groups characterising the structure of finitely generated abelian groups as a uniquely determined product of cyclic groups. Both the invariant factor decomposition and the primary decomposition are covered. Additionally, some results from the field of character groups are included, as well as work on formalising the direct product, the internal direct product and more group-theoretic lemmas – on both the newly introduced definitions and on already existing definitions from HOL-Algebra – the canonical Isabelle/HOL library on abstract algebra.

PDF Download

Student: Joseph Thommes

Supervisor: Manuel Eberl

Professor: Prof. Tobias Nipkow