A Formalization of Finite Group Theory: Part III

David M. Russinoff
(Arm Inc.)

This is the third and final installment of an exposition of an ACL2 formalization of finite group theory. Part I covers groups and subgroups, cosets, normal subgroups, and quotient groups. Part II extends the theory in the developmnent of group homomorphisms and direct products, which are applied in a proof of the Fundamental Theorem of Finite Abelian Groups. The central topics of the present paper are the symmetric groups and the Sylow theorems, which pertain to subgroups of prime power order. Since these theorems are based on the conjugation of subgroups, an example of a group action on a set, their presentation is preceded by a comprehensive treatment of group actions. Our final result is mainly an application of the Sylow theorems: after showing that the alternating group of order 60 is simple (i.e., has no proper normal subgroup), we prove that no group of non-prime order less than 60 is simple. The combined content of the groups directory is a close approximation to that of an advanced undergraduate course taught by the author in 1976.

In Alessandro Coglio and Sol Swords: Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2023), Austin, TX, USA and online, November 13-14, 2023, Electronic Proceedings in Theoretical Computer Science 393, pp. 33–49.
Published: 14th November 2023.

ArXived at: https://dx.doi.org/10.4204/EPTCS.393.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org