2026-07-26T00:58:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24603 2025-12-12T15:09:50Z ddc:004 open_access

A Formalization of Divided Powers in Lean Chambert-Loir, Antoine de Frutos-Fernández, María Inés Formal mathematics algebraic number theory commutative algebra divided powers Lean Mathlib 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Antoine Chambert-Loir and María Inés de Frutos-Fernández 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.4 urn:nbn:de:0030-drops-246038 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.4 eng https://creativecommons.org/licenses/by/4.0/legalcode