Theorem PadicInt.mahlerSeries_apply_nat

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.mahlerSeries_apply_natView on Github →