类型论中的形式化群
Formalizing groups in type theory
摘要：
在本文中，我们形式化的群论的一些基本概念和定理的类型论的一个变种称为构造与定义的演算。在这个理论中，我们引入了一个群的定义，它既一般又简单，足以用于形式证明。在此基础上，给出了子群、陪集、共轭、正规子群、商群等概念，并给出了相应的定理。我们的目标是保持这些形式化的透明和简洁，并尽可能接近标准的数学理论。结果可以实现在证明助手，是基于微积分的建设。
英文摘要：
In this paper we formalize some foundation concepts and theorems of group theory in a variant of type theory called the Calculus of Constructions with Definitions. In this theory we introduce definition of a group, which is both general and simple enough to use in formal proofs. Based on this definition, we formalize the concepts of subgroup, coset, conjugate, normal subgroup, and quotient group, and formally derive some related theorems. We aim to keep these formalizations transparent and concise, and as close as possible to the standard mathematical theory. The results can be implemented in proof assistants that are based on calculus of constructions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
