Theorem PadicInt.mahlerEquiv_symm_apply

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