Formal target: Corpus.Erdos416.erdos_416.parts.i

Let V(x) count the number of n≤x such that ϕ(m)=n is solvable.

Exact formal statement

Filter.Tendsto.{0, 0} (fun x => HDiv.hDiv.{0, 0, 0} (Corpus.Erdos416.V (HMul.hMul.{0, 0, 0} 2 x)) (Corpus.Erdos416.V x))
  Filter.atTop.{0} (nhds.{0} 2)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record