A formalization of divided powers in lean

DOI10.4230/LIPICS.ITP.2025.4MaRDI QIDQ7323647zbMATH OpenFDO

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

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.4

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A univalent formalization of the \(p\)-adic numbers
• Cohomologie cristalline des schemas de caractéristique \(p >0\)
• Commutative algebra in the Mizar system
• Formal power series
• Formalizing norm extensions and applications to number theory
• scientific article; zbMATH DE number 3233744 (Why is no real title available?)
• Lois polynomes et lois formelles en théorie des modules
• Notes on Crystalline Cohomology. (MN-21)
• Sur l'algèbre des puissances divisées d'un module et le module de ses différentielles
• The Lean 4 theorem prover and programming language
• The Lean theorem prover (system description)

This page was built for publication: A formalization of divided powers in lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323647)