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 statement7 of 9

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

FormalConjectures/ErdosProblems/700.leanErdos700.f_le1 lineExact file

1∀ (n k : ℕ), 1 < k → k ≤ n / 2 → Erdos700.f n ≤ n.gcd (n.choose k)

APIStatement only, no proof