cast_choose — Mathlib

English

Let a,b be natural numbers and K a division semiring of characteristic zero. If a ≤ b, then C(b,a) = b! / (a! (b−a)!).

Русский

Пусть a,b ∈ ℕ и K — деление кольцо характеристика ноль. При a ≤ b выполняется C(b,a) = b! / (a!(b−a)!).

LaTeX

$$$$ {b \\choose a} = \\frac{b!}{a!(b-a)!}. $$$$

Lean4

theorem cast_choose {a b : ℕ} (h : a ≤ b) : (b.choose a : K) = b ! / (a ! * (b - a)!) :=
  by
  have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (by positivity)
  rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
  rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]

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