有限群理论的形式化：第二部分
离散数学
2023-11-16 v1
摘要
本文是关于有限群理论 ACL2 形式化阐述的第二部分。第一部分于 2022 年 ACL2 研讨会上发表，涵盖了群与子群、陪集、正规子群和商群，并以柯西定理的证明作结：若群 G 的阶可被素数 p 整除，则 G 含有阶为 p 的元素。本续篇论述同态、直积以及有限阿贝尔群基本定理：每个有限阿贝尔群都同构于一列循环 p-群的直积，其阶在置换意义下唯一。该定理是 ACL2 的合适应用，因为它广泛依赖递归与归纳以及分解的构造性本质。唯一性的证明尤其具有挑战性，需要对通常被视为不言自明的模糊直觉进行形式化。
引用
@article{arxiv.2311.08866,
title = {A Formalization of Finite Group Theory: Part II},
author = {David M. Russinoff},
journal= {arXiv preprint arXiv:2311.08866},
year = {2023}
}
备注
In Proceedings ACL2-2023, arXiv:2311.08373