succ_dvd_centralBinom — Mathlib

English

(n+1) ∣ centralBinom(n).

Русский

(n+1) делит centralBinom(n).

LaTeX

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

Lean4

/-- A crucial lemma to ensure that Catalan numbers can be defined via their explicit formula
  `catalan n = n.centralBinom / (n + 1)`. -/
theorem succ_dvd_centralBinom (n : ℕ) : n + 1 ∣ n.centralBinom :=
  by
  have h_s : (n + 1).Coprime (2 * n + 1) :=
    by
    rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
    exact coprime_one_left n
  apply h_s.dvd_of_dvd_mul_left
  apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two
  rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]
  exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)

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