2022/03/06 by María Inés de Frutos-Fernández, de Frutos-Fernández, María Inés
Mathematics · #Algebraic Geometry and Number Theory #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Number Theory (math.NT)
paper · pdf · doi:10.48550/arxiv.2203.16344
openalex publication_date 2022/03/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.