mathlib documentation

data.nat.choose.dvd

Divisibility properties of binomial coefficients #

source
theorem nat.prime.dvd_choose_add {p a b : ℕ} (hap : a < p) (hbp : b < p) (h : p ≤ a + b) (hp : nat.prime p) :
p ∣ (a + b).choose a
source
theorem nat.prime.dvd_choose_self {p k : ℕ} (hk : 0 < k) (hkp : k < p) (hp : nat.prime p) :
p ∣ p.choose k