Current browse context:
cs.LO
Change to browse by:
References & Citations
Computer Science > Logic in Computer Science
Title: Formalizing the Ring of Adèles of a Global Field
(Submitted on 6 Mar 2022)
Abstract: The ring of ad\`eles of a global field and its group of units, the group of id\`eles, 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\`ele class group.
Submission history
From: María Inés De Frutos-Fernández [view email][v1] Sun, 6 Mar 2022 22:24:34 GMT (116kb,D)
Link back to: arXiv, form interface, contact.