Theorem 1.8: Fundamental Theorem of Algebra

Proved

Hatcher.fundamental_theorem_of_algebra

by korbonits · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologycovering-spacesfundamental-grouphatcher

Theorem 1.8. Every nonconstant polynomial with coefficients in $\mathbb{C}$ has a root in $\mathbb{C}$ :

f\in\mathbb{C}[z],\quad \deg f\ge 1\ \Longrightarrow\ \exists\,z\in\mathbb{C}:\ f(z)=0 .

Hatcher derives this from Theorem 1.7: if $f$ had no roots, the normalised loops $s\mapsto f(re^{2\pi i s})/|f(re^{2\pi i s})|$ would give a homotopy in $S^1$ from a constant loop to a loop homotopic to $\omega_n$ with $n=\deg f$ , forcing $n=0$ .

Formalization Note "Nonconstant" is $0<\deg f$ in Mathlib's Polynomial.degree, which excludes the zero polynomial (degree $\bot$ ) and nonzero constants (degree $0$ ). Mathlib already proves this statement as Complex.exists_root (via Liouville's theorem); it is recorded here as one of the section's stated theorems.

Preamble

import Definitions.Def_Hatcher_Circle
import Mathlib

open unitInterval Hatcher

Formal statement

namespace Hatcher
theorem fundamental_theorem_of_algebra (f : Polynomial ℂ) (hf : 0 < f.degree) :
    ∃ z : ℂ, f.IsRoot z := by sorry
end Hatcher

Source

A. Hatcher, Algebraic Topology, Cambridge University Press 2002, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Section 1.1, p. 31, Theorem 1.8

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Declaration Hatcher.fundamental_theorem_of_algebra.

Let $f$ be a polynomial with complex coefficients, $f \in \mathbb{C}[X]$ (Mathlib's Polynomial ℂ, i.e. a finitely supported function from exponents $n \in \mathbb{N}$ to coefficients in $\mathbb{C}$ ). The single hypothesis is

0 < \deg f,

where $\deg f$ is Mathlib's Polynomial.degree: it takes values in $\mathbb{N} \cup \{\bot\}$ (the naturals with an adjoined bottom element $\bot$ that is strictly smaller than every natural number), and is defined as the maximum exponent in the support of $f$ , with $\deg 0 = \bot$ . The inequality $0 < \deg f$ is the strict order of $\mathbb{N} \cup \{\bot\}$ , with $0$ denoting the natural number $0$ embedded there. Consequently the hypothesis excludes exactly the polynomials whose degree is $\bot$ or $0$ : the zero polynomial (degree $\bot$ ) and the nonzero constant polynomials (degree $0$ ). Every polynomial that is left has some monomial $X^n$ with $n \ge 1$ appearing with nonzero coefficient; the hypothesis is satisfiable (e.g. by $f = X$ ), so the statement is not vacuous.

The conclusion is

\exists\, z \in \mathbb{C},\quad f(z) = 0,

where Polynomial.IsRoot f z unfolds by definition to Polynomial.eval z f = 0, i.e. the evaluation of $f$ at $z$ — the sum $\sum_n a_n z^n$ over the coefficients $a_n$ of $f$ , computed in $\mathbb{C}$ with the identity ring homomorphism — equals $0 \in \mathbb{C}$ . The existential is plain existence ( $\exists$ ), not unique existence: nothing is asserted about how many roots there are, about multiplicities, about $f$ splitting into linear factors, or about any relation between the number of roots and $\deg f$ .

There are no other binders, implicit arguments, or typeclass assumptions beyond those built into $\mathbb{C}$ being a commutative ring (needed for Polynomial ℂ, degree, and eval). The theorem uses none of the custom definitions from the Hatcher namespace bundle (circleCover, omegaLoopN, omegaLoop, omegaClass); the open unitInterval Hatcher line brings names into scope but none are referenced in the statement.

Human review

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

View graph