English
Every nonconstant polynomial with complex coefficients has a root in ℂ.
Русский
Каждый ненулевой многочлен над комплексными числами имеет корень в К.
LaTeX
$$$$ \\forall p \\in \\mathbb{C}[X],\\ p \\text{ nonconstant } \\Rightarrow \\exists z \\in \\mathbb{C}, p(z)=0. $$$$
Lean4
/-- **Fundamental theorem of algebra**: every nonconstant complex polynomial
has a root. -/
theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z :=
by
by_contra! hf'
have (z : ℂ) : (f.eval z)⁻¹ = 0 :=
(f.differentiable.inv hf').apply_eq_of_tendsto_cocompact z <|
Metric.cobounded_eq_cocompact (α := ℂ) ▸
(Filter.tendsto_inv₀_cobounded.comp <| by
simpa only [tendsto_norm_atTop_iff_cobounded] using f.tendsto_norm_atTop hf tendsto_norm_cobounded_atTop)
-- Thus `f = 0`, contradicting the fact that `0 < degree f`.
obtain rfl : f = C 0 := Polynomial.funext fun z ↦ inv_injective <| by simp [this]
simp at hf
