mathlib documentation

data.nat.choose.dvd

Divisibility properties of binomial coefficients #

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
theorem nat.prime.dvd_choose_self {p k : } (hk : 0 < k) (hkp : k < p) (hp : nat.prime p) :
p p.choose k