Papers With

← All papers
First page of Fitting's Theorem and Semirings of Normal Subgroups

Fitting's Theorem and Semirings of Normal Subgroups

Damiano Testa

math.GR Jul 31, 2026 · v1 cs.LO
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
Fitting's theorem is reproved via a semiring structure on normal subgroups and fully formalized in Lean 4 using Mathlib.
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.
Problem

Fitting's classical theorem states that the join of two nilpotent normal subgroups of a group is nilpotent. The authors seek a new, ring-theoretic proof strategy and a machine-checked verification.

Approach

They define a non-unital, generally non-associative, commutative semiring on the normal subgroups of a group, with addition given by the join and multiplication by the subgroup commutator. Positive powers in this semiring coincide with terms of the lower central series. Fitting's theorem is then deduced from a nilpotence result for sums of nilpotent elements, using a binomial expansion in the non-associative setting. The entire development is formalized in Lean 4, leveraging Mathlib's algebraic and ordered hierarchies.

Results

They provide a NonUnitalNonAssocCommSemiring instance on NormalSubgroups(G) and formally prove Fitting's theorem, including the class bound h+k, all verified in Lean with Mathlib.