Commit 2025-10-14 19:24 bab341fd
View on Github →feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp (#26956)
We construct a divided power structure on the ideal (p) ⊆ ℤ_[p], given by the family of maps fun n x ↦ x^n / n!.
feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp (#26956)
We construct a divided power structure on the ideal (p) ⊆ ℤ_[p], given by the family of maps fun n x ↦ x^n / n!.