dvd_choose_add — Mathlib

English

Let p be a prime. If a < p, b < p, and p ≤ a + b, then p divides choose(a+b,a).

Русский

Пусть p простое. Если a < p, b < p и p ≤ a + b, то p делит C(a+b,a).

LaTeX

$$$$ p \\mid \\binom{a+b}{a}. $$$$

Lean4

theorem dvd_choose_add (hp : Prime p) (hap : a < p) (hbp : b < p) (h : p ≤ a + b) : p ∣ choose (a + b) a :=
  by
  have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h
  rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul, hp.dvd_factorial,
    hp.dvd_factorial] at h₁
  exact (h₁.resolve_right hbp.not_ge).resolve_right hap.not_ge

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