mathlib3 documentation

data.nat.choose.dvd

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