Abstract:This note discusses our formalisation in Lean 4 of the classification of groups of order $p^3$ for a prime number $p$, using mathlib4. We present the five isomorphism classes and give a detailed account of the formalisation, with particular emphasis on the non-abelian case, which requiring the most substantial formal development. For odd~$p$, the non-abelian groups are the Heisenberg group $\Heis(\Z/p\Z)$ and the semidirect product $\Z/p^2\Z\rtimes\Z/p\Z$; for $p=2$, they are $D_4$ and $Q_8$. We describe the construction of these concrete groups, the structural lemmas about centers, commutators, and exponents, and the explicit isomorphism constructions that classify an arbitrary non-abelian $p^3$-group.
From: Xiang Li [view email]
[v1]
Sat, 20 Jun 2026 12:41:33 UTC (12 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。