Erdős problem 700

`f n` is a lower bound: `f n ≤ gcd(n, C(n,k))` for every `1 < k ≤ n/2`.

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

700.lean

Retained formal statement9 of 9

Lucas (one step): for prime P ∣ n, if P ∤ C(n,k) then P ∣ k.

FormalConjectures/ErdosProblems/700.leanErdos700.prime_dvd_of_not_dvd_choose1 lineExact file

1∀ (P n k : ℕ), Nat.Prime P → P ∣ n → ¬P ∣ n.choose k → P ∣ k

APIStatement only, no proof