lean_workbook_plus_64842

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given positive integers $k$ and $m$ , show that $m$ and $\binom{n}{k}$ are coprime for infinitely many integers $n\geq k$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64842 (k m : ℕ) (h₁ : 0 < k ∧ 0 < m) (h₂ : m ≤ k) : ∃ n, n ≥ k ∧ Nat.Coprime m (Nat.choose n k)   :=  by sorry

Source