Def DividedPowers.DPMorphism.mk'

Modification history

2025-03-13 14:38
Mathlib/RingTheory/DividedPowers/DPMorphism.lean
feat(RingTheory/DividedPowers/DPMorphism): add divided power morphisms (#22318) …
Added DividedPowers.DPMorphism.mk'View on Github →