Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Finitely_Generated_Abelian_Groups


view this post on Zulip Email Gateway (Jul 13 2021 at 18:50):

From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new entry, Finitely Generated Abelian Groups, by Joseph Thommes and Manuel Eberl:

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.

It’s online at https://www.isa-afp.org/entries/Finitely_Generated_Abelian_Groups.html

And incidentally, we passed 600 articles some time ago. Keep them coming!

Larry Paulson


Last updated: Dec 05 2021 at 23:19 UTC