descFactorial_eq_factorial_mul_choose

English

For all n,k ∈ ℕ, the binomial coefficient equals the descending factorial divided by k!, i.e. C(n,k) = n descFactorial k / k!.

Русский

Для всех n,k ∈ ℕ биномиальный коэффициент равен нисходящему факториалу делённому на k!, то есть C(n,k) = n↓k / k!.

LaTeX

$$$$ \binom{n}{k} = \frac{n^{\downarrow k}}{k!} $$$$

Lean4

theorem descFactorial_eq_factorial_mul_choose (n k : ℕ) : n.descFactorial k = k ! * n.choose k :=
  by
  obtain h | h := Nat.lt_or_ge n k
  · rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]
  rw [Nat.mul_comm]
  apply Nat.mul_right_cancel (n - k).factorial_pos
  rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]

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