Erdős problem 1048
If is a monic polynomial with all roots satisfying for some , then must have a connected component with diameter ?
Sources
FormalConjectures/ErdosProblems/
1048.lean
Retained formal statement
If then the component which contains must have diameter , which shows is best possible.
∀ (n : ℕ), 1 ≤ n → Metric.ediam (connectedComponentIn (Erdos1043.levelSet (Polynomial.X ^ n)) 0) = 2SolvedStatement only, no proof