The fundamental theorem of algebra

D'Alembert and Argand's proof

theorem dalembert_lemma {p : Polynomial ℂ} (hp : p.natDegree > 0) {a : ℂ} (hpa : Polynomial.eval a p ≠ 0) {R : ℝ} (hR : 0 < R) : ∃ (b : ℂ), ‖b - a‖ < R ∧ ‖Polynomial.eval b p‖ < ‖Polynomial.eval a p‖

theorem fundamental_theorem_of_algebra (p : Polynomial ℂ) (hp : p.natDegree > 0) : ∃ (z : ℂ), Polynomial.eval z p = 0