Theorem PadicInt.norm_mahlerTerm

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