dvd_choose_self — Mathlib

English

Let p be a prime and k with 0 < k < p. Then p divides the binomial coefficient C(p, k).

Русский

Пусть p — простое число и 0 < k < p. Тогда p делит биномиальный коэффициент C(p, k).

LaTeX

$$$ p \\text{ is prime} \\land 0 < k \\land k < p \\Rightarrow p \\mid \\binom{p}{k}. $$$

Lean4

theorem dvd_choose_self (hp : Prime p) (hk : k ≠ 0) (hkp : k < p) : p ∣ choose p k :=
  hp.dvd_choose hkp (sub_lt ((zero_le _).trans_lt hkp) <| zero_lt_of_ne_zero hk) le_rfl

Похожие утверждения