English
For prime p and each k ∈ ℕ there exists a unique continuous map f_k: ℤ_p → ℤ_p such that f_k(n) = binomial(n,k) for all natural n.
Русский
Для простого p и каждого k ∈ ℕ существуют единственные непрерывные отображения f_k: ℤ_p → ℤ_p такие, что f_k(n) = {n \\choose k} для всех натуральных n.
LaTeX
$$$$ \\forall p \\text{ prime}, \\forall k \\in \\mathbb{N}, \\; \\exists! f_k: \\mathbb{Z}_p \\to \\mathbb{Z}_p \\text{ such that } f_k(n) = {n \\choose k} \\text{ for all } n \\in \\mathbb{N}. $$$$
Lean4
/-- The `k`-th Mahler basis function, i.e. the unique continuous function `ℤ_[p] → ℤ_[p]`
agreeing with `n ↦ n.choose k` for `n ∈ ℕ`. See [colmez2010], §1.2.1.
-/
noncomputable def mahler (k : ℕ) : C(ℤ_[p], ℤ_[p])
where
toFun x := Ring.choose x k
continuous_toFun := PadicInt.continuous_choose k
