Erdős problem 1041
Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If is a monic degree polynomial with all roots in the unit disk, then some connected component of contains at least two roots with multiplicity.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/1041.lean∀ (n : ℕ) (f : Polynomial ℂ), n ≥ 2 → f.natDegree = n → f.Monic → f.rootSet ℂ ⊆ Metric.ball 0 1 → ∃ z₁ z₂, ∃ (_ : {z₁, z₂} ≤ f.roots), ∃ γ, Set.range ⇑γ ⊆ {z | ‖Polynomial.eval z f‖ < 1} ∧ Erdos1041.length (Set.range ⇑γ) < 2OpenStatement only, no proof
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
AI collaborating with humans
- Machine
- People
AI standalone
- Machine