mathlib documentation

data.​nat.​choose

data.​nat.​choose

theorem nat.​prime.​dvd_choose_add {p a b : } :
a < pb < pp a + bnat.prime pp (a + b).choose a

theorem nat.​prime.​dvd_choose_self {p k : } :
0 < kk < pnat.prime pp p.choose k

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

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

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

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

theorem commute.​add_pow {α : Type u_1} [semiring α] {x y : α} (h : commute x y) (n : ) :
(x + y) ^ n = (finset.range (n + 1)).sum (λ (m : ), x ^ m * y ^ (n - m) * (n.choose m))

A version of the binomial theorem for noncommutative semirings.

theorem add_pow {α : Type u_1} [comm_semiring α] (x y : α) (n : ) :
(x + y) ^ n = (finset.range (n + 1)).sum (λ (m : ), x ^ m * y ^ (n - m) * (n.choose m))

The binomial theorem

theorem sum_range_choose (n : ) :
(finset.range (n + 1)).sum (λ (m : ), n.choose m) = 2 ^ n

The sum of entries in a row of Pascal's triangle

Specific facts about binomial coefficients and their sums

theorem sum_range_choose_halfway (m : ) :
(finset.range (m + 1)).sum (λ (i : ), (2 * m + 1).choose i) = 4 ^ m

theorem choose_middle_le_pow (n : ) :
(2 * n + 1).choose n 4 ^ n