License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.5
URN: urn:nbn:de:0030-drops-139004
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13900/
Go to the corresponding LIPIcs Volume Portal


Baanen, Anne ; Dahmen, Sander R. ; Narayanan, Ashvni ; Nuccio Mortarino Majno di Capriglio, Filippo A. E.

A Formalization of Dedekind Domains and Class Groups of Global Fields

pdf-format:
LIPIcs-ITP-2021-5.pdf (0.8 MB)


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.

BibTeX - Entry

@InProceedings{baanen_et_al:LIPIcs.ITP.2021.5,
  author =	{Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni and Nuccio Mortarino Majno di Capriglio, Filippo A. E.},
  title =	{{A Formalization of Dedekind Domains and Class Groups of Global Fields}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13900},
  URN =		{urn:nbn:de:0030-drops-139004},
  doi =		{10.4230/LIPIcs.ITP.2021.5},
  annote =	{Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib}
}

Keywords: formal math, algebraic number theory, commutative algebra, Lean, mathlib
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Full source code of the formalization is part of mathlib. Copies of the source files relevant to this paper are available in a separate repository.
Software: https://github.com/lean-forward/class-number archived at: https://archive.softwareheritage.org/swh:1:dir:3e46fd736dbb76b6e7be7f31ebc973f1a1c0237d


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI