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

Document
DOI: 10.4230/LIPIcs.ITP.2025.4
A Formalization of Divided Powers in Lean

Authors: Antoine Chambert-Loir and María Inés de Frutos-Fernández

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps {γ_n : I → A}_{n ∈ ℕ}, subject to axioms that imply that it behaves like the family {x ↦ xⁿ/n!}_{n ∈ ℕ}, but which can be defined even when division by factorials is not possible in A. Divided power structures have important applications in diverse areas of mathematics, including algebraic topology, number theory and algebraic geometry. In this article we describe a formalization in Lean 4 of the basic theory of divided power structures, including divided power morphisms and sub-divided power ideals, and we provide several fundamental constructions, in particular quotients and sums. This constitutes the first formalization of this theory in any theorem prover. As a prerequisite of general interest, we expand the formalized theory of multivariate power series rings, endowing them with a topology and defining evaluation and substitution of power series.
Cite as

Antoine Chambert-Loir and María Inés de Frutos-Fernández. A Formalization of Divided Powers in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chambertloir_et_al:LIPIcs.ITP.2025.4,
  author =	{Chambert-Loir, Antoine and de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s},
  title =	{{A Formalization of Divided Powers in Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{4:1--4:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.4},
  URN =		{urn:nbn:de:0030-drops-246038},
  doi =		{10.4230/LIPIcs.ITP.2025.4},
  annote =	{Keywords: Formal mathematics, algebraic number theory, commutative algebra, divided powers, Lean, Mathlib}
}
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 Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2021

  • Refine by Author
  • 1 Baanen, Anne
  • 1 Chambert-Loir, Antoine
  • 1 Dahmen, Sander R.
  • 1 Narayanan, Ashvni
  • 1 Nuccio Mortarino Majno di Capriglio, Filippo A. E.
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Mathematics of computing → Mathematical software
  • 1 Security and privacy → Logic and verification
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Lean
  • 2 algebraic number theory
  • 2 commutative algebra
  • 1 Formal mathematics
  • 1 Mathlib
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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