two_dvd_centralBinom_of_one_le

Mathlib.Data.Nat.Choose.Central

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

← MathLib Explorer

English

If n > 0, then 2 divides centralBinom(n).

Русский

Если n > 0, то 2 делит centralBinom(n).

LaTeX

$$$$ 2 \\mid \\binom{2n}{n} \\quad (n > 0). $$$$

Lean4

theorem two_dvd_centralBinom_of_one_le {n : ℕ} (h : 0 < n) : 2 ∣ centralBinom n :=
  by
  rw [← Nat.succ_pred_eq_of_pos h]
  exact two_dvd_centralBinom_succ n.pred

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

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

Разделы

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

Аффилиация

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