Commit 2026-03-30 09:56 00b8b594

View on Github →

doc(RingTheory/DividedPowerAlgebra/Init): adjust documentation and implicit variables (#37345) Address comments regarding documentation and implicit variables that were sent after #35804 was merged.

Estimated changes

modified inductive DividedPowerAlgebra.Rel
modified theorem DividedPowerAlgebra.dp_add
modified theorem DividedPowerAlgebra.dp_mul
modified theorem DividedPowerAlgebra.dp_null
modified theorem DividedPowerAlgebra.dp_smul
modified theorem DividedPowerAlgebra.dp_zero
modified theorem DividedPowerAlgebra.prod_dp