coprime_choose_of_lt — Mathlib

English

Let p be prime, b < p, and a ≤ b. Then p is coprime to C(b, a), i.e. gcd(p, C(b, a)) = 1.

Русский

Пусть p — простое число, b < p, и a ≤ b. Тогда p взаимно с C(b, a), то есть gcd(p, C(b, a)) = 1.

LaTeX

$$$ p \\text{ prime} \\land b

Lean4

theorem coprime_choose_of_lt (hp : p.Prime) (hb : b < p) (ha : a ≤ b) : p.Coprime (b.choose a) :=
  by
  rw [Nat.choose_eq_descFactorial_div_factorial]
  exact (hp.coprime_descFactorial_of_lt_of_le hb ha).coprime_div_right (Nat.factorial_dvd_descFactorial b a)

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