有限群理论的形式化：第三部分
离散数学
2023-11-16 v1
摘要
这是对ACL2形式化有限群理论阐述的第三也是最后一部分。第一部分涵盖群与子群、陪集、正规子群和商群。第二部分在群同态和直积的发展中扩展了该理论，并将其应用于有限阿贝尔群基本定理的证明。本文的中心主题是对称群和Sylow定理，后者涉及素数幂阶子群。由于这些定理基于子群的共轭（群在集合上作用的一个例子），在呈现它们之前先对群作用进行了全面处理。我们的最终结果主要是Sylow定理的一个应用：在证明60阶交错群是单群（即无真正规子群）之后，我们证明阶小于60的非素数阶群均非单群。groups目录的综合内容近似于作者1976年所授高级本科课程的内容。
引用
@article{arxiv.2311.08854,
title = {A Formalization of Finite Group Theory: Part III},
author = {David M. Russinoff},
journal= {arXiv preprint arXiv:2311.08854},
year = {2023}
}
备注
In Proceedings ACL2-2023, arXiv:2311.08373