2026-08-17T09:55:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16723 2024-03-06T10:58:09Z ddc:004 open_access

Formalizing the Ring of Adèles of a Global Field de Frutos-Fernández, María Inés formal math algebraic number theory class field theory Lean mathlib 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 formalize 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik María Inés de Frutos-Fernández 2022 Is Part Of LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2022.14 urn:nbn:de:0030-drops-167232 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.14 eng https://creativecommons.org/licenses/by/4.0/legalcode