Prove2Me

Algebraic elements over an algebraically closed field are constants

Proved
OAI.PiExponent.FormalInterpolation.isAlgebraic_eq_algebraMap_of_isAlgClosed

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

If E is a field extension of the complex numbers and x in E is algebraic over C, then x lies in the image of the structure map C → E, since C is algebraically closed.

Preamble
import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Data.Complex.Basic
Formal statement
theorem OAI.PiExponent.FormalInterpolation.isAlgebraic_eq_algebraMap_of_isAlgClosed
    {E : Type} [Field E] [Algebra Complex E] (x : E) (hx : IsAlgebraic Complex x) :
    ∃ a : Complex, x = algebraMap Complex E a := by sorry
Source
Mathlib IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic.

View graph