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
theorem nat.choose_eq_factorial_div_factorial' {a b : } (hab : a b) :
(b.choose a) = b! / (a!) * (b - a)!
theorem nat.choose_mul {n k s : } (hn : k n) (hs : s k) :
((n.choose k)) * (k.choose s) = ((n.choose s)) * ((n - s).choose (k - s))