Theorem 8.8 — the fundamental theorem of algebra

Proved

Rudin.ch08_fundamental_theorem_of_algebra

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraanalysis

If $a_0, \dots, a_n$ are complex numbers with $n \ge 1$ and $a_n \ne 0$ , then $\sum_{k=0}^{n} a_k z^k = 0$ for some complex $z$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.8 (fundamental theorem of algebra): every nonconstant complex polynomial
has a root. -/
theorem ch08_fundamental_theorem_of_algebra (n : ℕ) (hn : 1 ≤ n) (a : ℕ → ℂ) (han : a n ≠ 0) :
    ∃ z : ℂ, ∑ k ∈ Finset.range (n + 1), a k * z ^ k = 0 := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 184, Theorem 8.8

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $n$ be a natural number with $n \ge 1$ , and let $a : \mathbb{N}\to\mathbb{C}$ be a family of complex coefficients with $a_n \ne 0$ . Then there exists $z \in \mathbb{C}$ with

\sum_{k=0}^{n} a_k z^{k} \;=\; 0 .

The sum runs over $k = 0,\dots,n$ inclusive, so the polynomial has degree exactly $n \ge 1$ because its leading coefficient $a_n$ is nonzero; coefficients $a_k$ for $k > n$ are present in the data but do not occur in the sum. Only the existence of one root is asserted — nothing about multiplicity, the number of roots, or factorization.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph