continuous_multichoose — Mathlib

English

Let p be a prime. For every k ∈ ℕ the map x ↦ binomial(x,k) from the p-adic integers ℤ_p to itself is continuous.

Русский

Пусть p — простое число. Для каждого k ∈ ℕ отображение x ↦ \n\\binom{x}{k} из p-адических целых \\mathbb{Z}_p в \\mathbb{Z}_p непрерывно.

LaTeX

$$$\\\\forall p \;\\text{prime}, \\\\forall k \\\\in \\\\(\\\\mathbb{N}, \\\\; x \\\\mapsto \\\\binom{x}{k} : \\\\mathbb{Z}_p \to \\\\mathbb{Z}_p \\\\text{ is continuous}. $$$

Lean4

@[fun_prop]
theorem continuous_multichoose (k : ℕ) : Continuous (fun x : ℤ_[p] ↦ Ring.multichoose x k) :=
  by
  simp only [Ring.multichoose, BinomialRing.multichoose, continuous_induced_rng]
  fun_prop

Похожие утверждения