mathlib3 documentation

data.nat.choose.cast

Cast of binomial coefficients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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))
source
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))
source
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)
source
theorem nat.cast_choose_two (K : Type u_1) [division_ring K] [char_zero K] (a : ℕ) :
↑(a.choose 2) = ↑a * (↑a - 1) / 2