1 Search Results for "Nuccio Mortarino Majno di Capriglio, Filippo A. E."

Document
DOI: 10.4230/LIPIcs.ITP.2021.5
A Formalization of Dedekind Domains and Class Groups of Global Fields

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

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

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.
Cite as

Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2021.5},
  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}
}
  • Refine by Author
  • 1 Baanen, Anne
  • 1 Dahmen, Sander R.
  • 1 Narayanan, Ashvni
  • 1 Nuccio Mortarino Majno di Capriglio, Filippo A. E.

  • Refine by Classification

  • Refine by Keyword
  • 1 Lean
  • 1 algebraic number theory
  • 1 commutative algebra
  • 1 formal math
  • 1 mathlib

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact