3 papers
cs.LO2025
Formalizing Polynomial Laws and the Universal Divided Power Algebra
Antoine Chambert-Loir, María Inés de Frutos-Fernández
The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/Mathlib mathematical library, of the construction by Roby (1965) of the univers…
cs.LO2025
A Formalization of Divided Powers in Lean
Antoine Chambert-Loir, María Inés de Frutos-Fernández
Given an ideal in a commutative ring , a divided power structure on is a collection of maps , subject to axioms that imply tha…
math.HO2023
Balade newtonienne entre analyse et arithmétique (Newtonian promenade between analysis and arithmetic)
Antoine Chambert-Loir
Invented by Kurt Hensel at the very end of 19th century on the model of power series in one indeterminate, the -adic numbers have not only become an indispensable tool of contem…