cast_choose_eq_descPochhammer_div

English

In a division ring K with CharZero, for a,b ∈ ℕ, C(a,b) = (descPochhammer K b).eval a / b!.

Русский

В кольце(K) делимости с характеристикой ноль, для a,b ∈ ℕ есть C(a,b) = (descPochhammer K b).eval a / b!.

LaTeX

$$$$ \\binom{a}{b} = \\frac{a(a-1)\\cdots (a-b+1)}{b!}. $$$$

Lean4

theorem cast_choose_eq_descPochhammer_div (a b : ℕ) : (a.choose b : K) = (descPochhammer K b).eval ↑a / b ! := by
  rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul, mul_comm, ←
    descFactorial_eq_factorial_mul_choose, descPochhammer_eval_eq_descFactorial]

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