Erdős problem 1000
Let be an infinite sequence of integers, and let count the number of such that the fraction does not have denominator for when written in lowest form; equivalently, for all .
Sources
FormalConjectures/ErdosProblems/
1000.lean
Retained formal statement
It is trivial that , where is the Euler totient function.
∀ (n : ℕ → ℕ), StrictMono n → ∀ (k : ℕ), (n k).totient ≤ Erdos1000.phiSeq n kSolvedStatement only, no proof