论文标题
正式化全球领域的阿德利斯环
Formalizing the Ring of Adèles of a Global Field
论文作者
论文摘要
全球领域及其单位群体的阿德尔（Adèles）圈，伊德尔斯（Idèles）是现代数字理论的基本对象。我们在精益3定理供奉献中讨论其定义的形式化。作为先决条件，我们对Dedekind领域进行了正式的ADIC估值。我们提出了一些应用程序，包括全球类字段理论的主要定理的说明，以及一个数字字段的理想班级组与其Idèle类组的明确商同构。
The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalized adic valuations on Dedekind domains. We present some applications, including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idèle class group.
