choose_eq_asc_factorial_div_factorial'

English

For all n,k ∈ ℕ, (n + k − 1) choose k equals n ascFactorial k divided by k!, i.e. C(n+k−1,k) = n ascFactorial k / k!.

Русский

Для всех n,k ∈ ℕ верно: C(n+k−1,k) = n ascFactorial k / k!.

LaTeX

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

Lean4

theorem choose_eq_asc_factorial_div_factorial' (n k : ℕ) : (n + k - 1).choose k = n.ascFactorial k / k ! :=
  Nat.eq_div_of_mul_eq_right k.factorial_ne_zero (ascFactorial_eq_factorial_mul_choose' _ _).symm

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