Documentation

Mathlib.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) [DivisionRing K] [CharZero 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) [DivisionRing K] [CharZero K] {a : } {b : } :
((a + b).choose a) = (a + b).factorial / (a.factorial * b.factorial)
theorem Nat.cast_choose_eq_ascPochhammer_div (K : Type u_1) [DivisionRing K] [CharZero K] (a : ) (b : ) :
(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / b.factorial
theorem Nat.cast_choose_two (K : Type u_1) [DivisionRing K] [CharZero K] (a : ) :
(a.choose 2) = a * (a - 1) / 2