Theorem PadicInt.coe_sum

Modification history

2025-10-14 19:24
Mathlib/NumberTheory/Padics/PadicIntegers.lean
feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp (#26956) …
Added PadicInt.coe_sumView on Github →