mathlib documentation

data.​nat.​choose

data.​nat.​choose

theorem nat.​prime.​dvd_choose_add {p a b : ℕ} :
a < p → b < p → p ≤ a + b → nat.prime p → p ∣ (a + b).choose a

theorem nat.​prime.​dvd_choose_self {p k : ℕ} :
0 < k → k < p → nat.prime p → p ∣ p.choose k

theorem choose_le_succ_of_lt_half_left {r n : ℕ} :
r < n / 2 → n.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