two_dvd_centralBinom_succ

Mathlib.Data.Nat.Choose.Central

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

← MathLib Explorer

English

For all n, 2 divides centralBinom(n+1).

Русский

Для любого n 2 делит centralBinom(n+1).

LaTeX

$$$$ 2 \\mid \\binom{2(n+1)}{n+1}. $$$$

Lean4

theorem two_dvd_centralBinom_succ (n : ℕ) : 2 ∣ centralBinom (n + 1) :=
  by
  use (n + 1 + n).choose n
  rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc, choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]

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

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

Разделы

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

Аффилиация

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