A formalization of Dedekind domains and class groups of global fields
Logic in Computer Science
2022-08-31 v4 Number Theory
Abstract
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.
Keywords
Cite
@article{arxiv.2102.02600,
title = {A formalization of Dedekind domains and class groups of global fields},
author = {Anne Baanen and Sander R. Dahmen and Ashvni Narayanan and Filippo A. E. Nuccio},
journal= {arXiv preprint arXiv:2102.02600},
year = {2022}
}
Comments
Expanded version of https://drops.dagstuhl.de/opus/volltexte/2021/13900/ (appeared ar in the Leibniz International Proceedings in Informatics - Conference Interactive Theorem Proving 2021 (Rome, Italy)). To appear in the Journal of Automated Reasoning