mathlib documentation

data.nat.choose.cast

Cast of binomial coefficients #

This file allows calculating the binomial coefficient a.choose b as an element of a division ring of characteristic 0.

theorem nat.cast_choose (K : Type u_1) [division_ring K] [char_zero K] {a b : ℕ} (h : a ≤ b) :

↑(b.choose a) = ↑(b.factorial) / (↑(a.factorial) * ↑((b - a).factorial))

theorem nat.cast_add_choose (K : Type u_1) [division_ring K] [char_zero K] {a b : ℕ} :

↑((a + b).choose a) = ↑((a + b).factorial) / (↑(a.factorial) * ↑(b.factorial))

theorem nat.cast_choose_eq_pochhammer_div (K : Type u_1) [division_ring K] [char_zero K] (a b : ℕ) :

↑(a.choose b) = polynomial.eval ↑(a - (b - 1)) (pochhammer K b) / ↑(b.factorial)

theorem nat.cast_choose_two (K : Type u_1) [division_ring K] [char_zero K] (a : ℕ) :

↑(a.choose 2) = ↑a * (↑a - 1) / 2