2026-07-22T04:20:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13900 2024-03-06T10:53:05Z ddc:004 open_access

A Formalization of Dedekind Domains and Class Groups of Global Fields Baanen, Anne Dahmen, Sander R. Narayanan, Ashvni Nuccio Mortarino Majno di Capriglio, Filippo A. E. formal math algebraic number theory commutative algebra Lean mathlib Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib’s decentralized collaboration processes involved in this project. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Anne Baanen and Sander R. Dahmen and Ashvni Narayanan and Filippo A. E. Nuccio Mortarino Majno di Capriglio 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.5 urn:nbn:de:0030-drops-139004 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5 eng https://creativecommons.org/licenses/by/4.0/legalcode