Theorem PadicInt.hasSum_mahlerSeries

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_mahlerSeriesView on Github →