Non-real roots of a real polynomial come in conjugate pairs

Proved

MetodosNumericos.conjugate_root

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

numerical-analysispolynomials

If $P$ has real coefficients and $z \\in \\mathbb{C}$ satisfies $P(z) = 0$ , then $P(\\bar{z}) = 0$ . This is Proposição 4.1.1; together with the fundamental theorem of algebra it says that the non-real roots of a real polynomial occur in conjugate pairs.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_polinomiosDefs

Formal statement

namespace MetodosNumericos

theorem conjugate_root (a : ℕ → ℝ) (n : ℕ) (z : ℂ) (hz : polyValC a n z = 0) :
    polyValC a n (starRingEnd ℂ z) = 0 := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 4, Proposição 4.1.1, p. 73.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

For an arbitrary function $a : \\mathbb{N} \\to \\mathbb{R}$ , an arbitrary natural number $n$ (including $n = 0$ ) and an arbitrary complex number $z$ , the statement assumes

\\sum_{i=0}^{n} a_i\\, z^{\\,n-i} = 0

and concludes

\\sum_{i=0}^{n} a_i\\, \\overline{z}^{\\,n-i} = 0,

where $\\overline{z}$ is the complex conjugate of $z$ and the coefficients are the same real numbers coerced into $\\mathbb{C}$ . No non-degeneracy hypothesis is imposed: if all the $a_i$ with $i \\le n$ vanish, both sides are $0$ and the implication is trivially true.

Human review

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

View graph