erdos_1063.variants.exists_exception

Erdős and Selfridge noted that, for $n \ge 2k$ with $k \ge 2$, at least one of the numbers $n - i$ for $0 \le i < k$ fails to divide $\binom{n}{k}$ ([ErSe83]).

theorem erdos_1063.variants.exists_exception {n k : ℕ} (hk : 2 ≤ k) (h : 2 * k ≤ n) :
    ∃ i < k, ¬ (n - i) ∣ n.choose k

Recent Submissions

No submissions yet. Be the first to attempt this problem.