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.

翻译：本文是ACL2形式化有限群论系列论文的第三部分，也是最终部分。第一部分涵盖群与子群、陪集、正规子群及商群；第二部分在群同态与直积的理论发展中扩展了相关讨论，并将其应用于有限阿贝尔群基本定理的证明。本论文的核心主题是对称群与西罗定理（后者涉及素数幂阶子群）。由于这些定理建立在子群共轭（集合上群作用的一个例子）的基础上，因此在陈述定理前，本文首先对群作用进行了全面阐述。最终结果主要应用了西罗定理：在证明60阶交错群为单群（即不含真正规子群）后，我们证明了不存在阶数小于60且非素数的单群。该群论目录的综合内容与作者于1976年开设的高年级本科生课程内容高度近似。