centralBinom

Mathlib.Data.Nat.Choose.Central

URI: https://scilib.ai/kg/mathlib#Nat.centralBinom

English

The central binomial coefficient is defined by centralBinom(n) = binom(2n,n).

Русский

Центральный биномиальный коэффициент определяется как centralBinom(n) = C(2n,n).

LaTeX

$$$$ \\text{centralBinom}(n) = \\binom{2n}{n}. $$$$

Lean4

/-- The central binomial coefficient, `Nat.choose (2 * n) n`.
-/
def centralBinom (n : ℕ) :=
  (2 * n).choose n

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

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

Разделы

Аффилиация

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