dvd_choose — Mathlib

English

Let p be a prime. If a < p, b - a < p, and p ≤ b, then p divides the binomial coefficient C(b, a).

Русский

Пусть p — простое число. Если a < p, b − a < p и p ≤ b, то p делит биномиальный коэффициент C(b, a).

LaTeX

$$$ p \\text{ is prime} \\land a

Lean4

theorem dvd_choose (hp : Prime p) (ha : a < p) (hab : b - a < p) (h : p ≤ b) : p ∣ choose b a :=
  have : a + (b - a) = b := Nat.add_sub_of_le (ha.le.trans h)
  this ▸ hp.dvd_choose_add ha hab (this.symm ▸ h)

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