Theorem PadicInt.hasSum_mahler

Modification history

2024-11-28 17:22
Mathlib/NumberTheory/Padics/MahlerBasis.lean
feat(NumberTheory/Padics): Mahler's theorem on continuous p-adic functions (#19473) …
Added PadicInt.hasSum_mahlerView on Github →