Antoine Chambert-Loir

collaborators

2 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

Given an ideal $I$ in a commutative ring $A$ , a divided power structure on $I$ is a collection of maps ${I^_{n}^{3} : I \to A}_{n \in N}$ , subject to axioms that imply th…