Theorem DividedPowers.DPMorphism.coe_toRingHom

Modification history

2025-03-13 14:38

Mathlib/RingTheory/DividedPowers/DPMorphism.lean

feat(RingTheory/DividedPowers/DPMorphism): add divided power morphisms (#22318) …

Added DividedPowers.DPMorphism.coe_toRingHom View on Github →