cast_choose_eq_ascPochhammer_div — Mathlib

English

In a division ring K with characteristic zero, for a,b ∈ ℕ, C(a,b) = (ascPochhammer K b).eval (a − (b − 1)) / b!.

Русский

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

LaTeX

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

Lean4

theorem cast_choose_eq_ascPochhammer_div (a b : ℕ) : (a.choose b : K) = (ascPochhammer K b).eval ↑(a - (b - 1)) / 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, ← cast_descFactorial]

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