Fitting's Theorem and Semirings of Normal Subgroups

Abstract

We define a non-unital, generally non-associative, commutative semiring structure on the collection of normal subgroups of a group $G$. This viewpoint allows us to recast in ring-theoretic terms Fitting's classical theorem that the join of two nilpotent normal subgroups is nilpotent. From this perspective, the two key inputs are a binomial expansion in a non-associative setting and the fact that the commutator subgroup of two normal subgroups lies in each factor. The development is formalized in Lean, making essential use of Mathlib for the core definitions and results.

Disclosure

“5 Thomas Browning, Inna Capdeboscq, Jireh Loreaux, Dmitriy Rumynin and Gareth Tracey. AI usage. Aristotle [Aristotle25] was used to find alternative proofs. Some of that code was reused in the final version. Claude Opus 5 [Claude26] was used during revision, to help streamline the text and the Lean code, and to add the finishing touches. References [Aristotle25] Tudor Achim et al. Aristotle: IMO-level Automated Theorem”

PDF page 5

Classification

Rewriting existing author-written text

Multiplier

4

Verified

2026-08-23T19:16:06.341271Z

Structural counts