mathlib documentation

data.nat.choose.basic

Binomial coefficients

This file contains a definition of binomial coefficients and simple lemmas (i.e. those not requiring more imports).

Main definition and results

def nat.choose  :

choose n k is the number of k-element subsets in an n-element set. Also known as binomial coefficients.

Equations
@[simp]
theorem nat.choose_zero_right (n : ) :
n.choose 0 = 1

@[simp]
theorem nat.choose_zero_succ (k : ) :
0.choose k.succ = 0

theorem nat.choose_succ_succ (n k : ) :

theorem nat.choose_eq_zero_of_lt {n k : } :
n < kn.choose k = 0

@[simp]
theorem nat.choose_self (n : ) :
n.choose n = 1

@[simp]
theorem nat.choose_succ_self (n : ) :
n.choose n.succ = 0

@[simp]
theorem nat.choose_one_right (n : ) :
n.choose 1 = n

theorem nat.triangle_succ (n : ) :
(n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

theorem nat.choose_two_right (n : ) :
n.choose 2 = n * (n - 1) / 2

choose n 2 is the n-th triangle number.

theorem nat.choose_pos {n k : } :
k n0 < n.choose k

theorem nat.succ_mul_choose_eq (n k : ) :
(n.succ) * n.choose k = (n.succ.choose k.succ) * k.succ

theorem nat.choose_mul_factorial_mul_factorial {n k : } :
k n((n.choose k) * k!) * (n - k)! = n!

theorem nat.choose_eq_factorial_div_factorial {n k : } :
k nn.choose k = n! / k! * (n - k)!

theorem nat.factorial_mul_factorial_dvd_factorial {n k : } :
k nk! * (n - k)! n!

@[simp]
theorem nat.choose_symm {n k : } :
k nn.choose (n - k) = n.choose k

theorem nat.choose_symm_of_eq_add {n a b : } :
n = a + bn.choose a = n.choose b

theorem nat.choose_symm_add {a b : } :
(a + b).choose a = (a + b).choose b

theorem nat.choose_symm_half (m : ) :
(2 * m + 1).choose (m + 1) = (2 * m + 1).choose m

theorem nat.choose_succ_right_eq (n k : ) :
(n.choose (k + 1)) * (k + 1) = (n.choose k) * (n - k)

@[simp]
theorem nat.choose_succ_self_right (n : ) :
(n + 1).choose n = n + 1

theorem nat.choose_mul_succ_eq (n k : ) :
(n.choose k) * (n + 1) = ((n + 1).choose k) * (n + 1 - k)

Inequalities

theorem nat.choose_le_succ_of_lt_half_left {r n : } :
r < n / 2n.choose r n.choose (r + 1)

Show that nat.choose is increasing for small values of the right argument.

theorem nat.choose_le_middle (r n : ) :
n.choose r n.choose (n / 2)

choose n r is maximised when r is n/2.