  This is the second installment of an exposition of an ACL2 formalization of
finite group theory. The first, which was presented at the 2022 ACL2 workshop,
covered groups and subgroups, cosets, normal subgroups, and quotient groups,
culminating in a proof of Cauchy's Theorem: If the order of a group G is
divisible by a prime p, then G has an element of order p. This sequel addresses
homomorphisms, direct products, and the Fundamental Theorem of Finite Abelian
Groups: Every finite abelian group is isomorphic to the direct product of a
list of cyclic p-groups, the orders of which are unique up to permutation. This
theorem is a suitable application of ACL2 because of its extensive reliance on
recursion and induction as well as the constructive nature of the
factorization. The proof of uniqueness is especially challenging, requiring the
formalization of vague intuition that is commonly taken as self-evident.
