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.

Estimated changes

Modified Mathlib/NumberTheory/Padics/MahlerBasis.lean

added theorem PadicInt.fwdDiff_mahlerSeries

added theorem PadicInt.hasSum_mahler

added theorem PadicInt.hasSum_mahlerSeries

added theorem PadicInt.mahlerEquiv_apply

added theorem PadicInt.mahlerEquiv_symm_apply

added theorem PadicInt.mahlerSeries_apply

added theorem PadicInt.mahlerSeries_apply_nat

added theorem PadicInt.mahlerTerm_apply

added theorem PadicInt.norm_mahlerTerm