choose_eq_factorial_div_factorial

English

For all n ≥ k, C(n,k) = n! / (k! (n-k)!).

Русский

Для всех n ≥ k биномиальный коэффициент C(n,k) равен n!/(k!(n-k)!).

LaTeX

$$$\\\\binom{n}{k} = \\\\dfrac{n!}{k! (n-k)!}$$$

Lean4

theorem choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) : choose n k = n ! / (k ! * (n - k)!) :=
  by
  rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]
  exact (mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm

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