Divisibility properties of binomial coefficients #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem nat.prime.dvd_choose_add {p a b : ℕ} (hp : nat.prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) :

p ∣ (a + b).choose a

theorem nat.prime.dvd_choose {p a b : ℕ} (hp : nat.prime p) (ha : a < p) (hab : b - a < p) (h : p ≤ b) :

theorem nat.prime.dvd_choose_self {p k : ℕ} (hp : nat.prime p) (hk : k ≠ 0) (hkp : k < p) :