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.
Student: Joseph Thommes
Supervisor: Manuel Eberl
Professor: Prof. Tobias Nipkow