Documentation

Mathlib.Data.Nat.Choose.Dvd

Divisibility properties of binomial coefficients #

theorem Nat.Prime.dvd_choose_add {p : } {a : } {b : } (hp : p.Prime) (hap : a < p) (hbp : b < p) (h : p a + b) :
p (a + b).choose a
theorem Nat.Prime.dvd_choose {p : } {a : } {b : } (hp : p.Prime) (ha : a < p) (hab : b - a < p) (h : p b) :
p b.choose a
theorem Nat.Prime.dvd_choose_self {p : } {k : } (hp : p.Prime) (hk : k 0) (hkp : k < p) :
p p.choose k