Erdős problem 304
Is it true that ?
Sources
FormalConjectures/ErdosProblems/
304.lean
Retained formal statement
∀ {a b : ℕ}, 1 ∈ Erdos304.unitFractionExpressible a b → ∃ m, 1 < m ∧ ↑a / ↑b = (↑m)⁻¹APIStatement only, no proof
Erdős problem 304
The source's own material, retained exactly.
16 retained statements · 36c6d0fef71a
Open selected sourceFormalConjectures/ErdosProblems/
304.lean
1∀ {a b : ℕ}, 1 ∈ Erdos304.unitFractionExpressible a b → ∃ m, 1 < m ∧ ↑a / ↑b = (↑m)⁻¹