erdos_694.variants.inf_unique

Erdős has proved that if there exists an integer $n$ for which $\phi(m) = n$ has exactly one solution, then there must be infinitely many such $n$.

theorem erdos_694.variants.inf_unique (h : ∃ n > 0, ∃! m, Nat.totient m = n) :
    { n | ∃! m, Nat.totient m = n }.Infinite

Recent Submissions

No submissions yet. Be the first to attempt this problem.