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! / (a!) * (b - a)!
theorem nat.cast_add_choose (K : Type u_1) [division_ring K] [char_zero K] {a b : } :
((a + b).choose a) = (a + b)! / (a!) * b!
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!
theorem nat.cast_choose_two (K : Type u_1) [division_ring K] [char_zero K] (a : ) :
(a.choose 2) = (a) * (a - 1) / 2