Divided powers in Lean Implementation of divided powers in Lean, by María Inés De Frutos Fernández and Antoine Chambert-Loir, 2022