choose_eq_asc_factorial_div_factorial

English

Let n,k be natural numbers. Then the binomial coefficient (n+k choose k) equals the rising factorial of length k starting at n+1 divided by k!, i.e. C(n+k,k) = (n+1) ascFactorial k / k!.

Русский

Пусть n, k ∈ ℕ. Тогда биномиальный коэффициент (n+k choose k) равен восходящему факториалу длины k, начинающемуся с n+1, делённому на k!, то есть C(n+k,k) = (n+1) ascFactorial k / k!.

LaTeX

$$$$ \binom{n+k}{k} = \frac{(n+1)^{\uparrow k}}{k!} $$$$

Lean4

theorem choose_eq_asc_factorial_div_factorial (n k : ℕ) : (n + k).choose k = (n + 1).ascFactorial k / k ! :=
  by
  apply Nat.mul_left_cancel k.factorial_pos
  rw [← ascFactorial_eq_factorial_mul_choose]
  exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm

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