centralBinom_eq_two_mul_choose

Mathlib.Data.Nat.Choose.Central

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

English

For all n, centralBinom(n) = binom(2n,n).

Русский

Для всех n выполняется centralBinom(n) = C(2n,n).

LaTeX

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

Lean4

theorem centralBinom_eq_two_mul_choose (n : ℕ) : centralBinom n = (2 * n).choose n :=
  rfl

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

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

Разделы

Аффилиация

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