Theorem PadicInt.coe_dpow_eq

Modification history

2025-10-14 19:24

Mathlib/RingTheory/DividedPowers/Padic.lean

feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp (#26956) …

Added PadicInt.coe_dpow_eq View on Github →