Erdős problem 677
Denote by the least common multiple of the finite set . Is it true that for all , we get ?
Sources
FormalConjectures/ErdosProblems/
677.lean
Retained formal statement
Denote by the least common multiple of the finite set . Is it true that for all , we get ?
∀ (m n k : ℕ), k > 0 → m ≥ n + k → Finset.lcmInterval m k ≠ Finset.lcmInterval n kOpenStatement only, no proof