Commit 2026-03-28 14:33 5308bb72

View on Github →

feat(RingTheory/DividedPowerAlgebra/Init): add universal divided power algebra (#35804) We define the universal divided power algebra of an R-module M. Co-authored by @AntoineChambert-Loir

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DividedPowerAlgebra/Init.lean

added inductive DividedPowerAlgebra.Rel

added def DividedPowerAlgebra.RelI

added theorem DividedPowerAlgebra.algHom_ext

added theorem DividedPowerAlgebra.algHom_ext_iff

added def DividedPowerAlgebra.dp

added theorem DividedPowerAlgebra.dp_add

added theorem DividedPowerAlgebra.dp_def

added theorem DividedPowerAlgebra.dp_eq_mkRingHom

added theorem DividedPowerAlgebra.dp_mul

added theorem DividedPowerAlgebra.dp_null

added theorem DividedPowerAlgebra.dp_null_of_ne_zero

added theorem DividedPowerAlgebra.dp_smul

added theorem DividedPowerAlgebra.dp_sum

added theorem DividedPowerAlgebra.dp_sum_smul

added theorem DividedPowerAlgebra.dp_zero

added def DividedPowerAlgebra.embed

added theorem DividedPowerAlgebra.embed_def

added theorem DividedPowerAlgebra.mkAlgHom_C

added theorem DividedPowerAlgebra.mkAlgHom_surjective

added theorem DividedPowerAlgebra.mkRingHom_C

added theorem DividedPowerAlgebra.natFactorial_mul_dp_eq

added theorem DividedPowerAlgebra.prod_dp

added theorem DividedPowerAlgebra.submodule_span_prod_dp_eq_top