mahler_natCast_eq

Mathlib.NumberTheory.Padics.MahlerBasis

URI: https://scilib.ai/kg/mathlib#mahler_natCast_eq

← MathLib Explorer

English

For any k ∈ ℕ and n ∈ ℕ, mahler k (n) = binomial(n,k).

Русский

Для любых k, n ∈ ℕ верно mahler(k, n) = {n \\choose k}.

LaTeX

$$$$ mahler(k, n) = {n \\choose k}, \\quad n \\in \\mathbb{N}. $$$$

Lean4

/-- The function `mahler k` extends `n ↦ n.choose k` on `ℕ`. -/
theorem mahler_natCast_eq (k n : ℕ) : mahler k (n : ℤ_[p]) = n.choose k := by
  simp only [mahler_apply, Ring.choose_natCast]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru