AI 中文总结
该研究在群的正规子群集合上定义非单位非结合交换半环结构，以环论术语重述菲廷定理，在Lean中结合Mathlib完成形式化，为群论定理提供了代数视角的形式化证明。
AI 中文摘要
我们在群G的正规子群集合上定义了一个非单位元、通常非结合、交换的半环结构。这一视角使我们能以环论术语重述菲廷的经典定理：两个幂零正规子群的并仍是幂零的。从该视角出发，两个关键输入是：非结合环境下的二项式展开，以及两个正规子群的换位子群包含于每个因子的事实。该发展在Lean中形式化，核心定义与结果关键使用了Mathlib。
英文摘要
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.
