Commit 2024-11-28 17:22 97bd49d5
View on Github →feat(NumberTheory/Padics): Mahler's theorem on continuous p-adic functions (#19473) This PR completes the proof of Mahler's theorem, showing that the Mahler functions give a Banach space basis for the continuous functions on Z_p.