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.

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