Non-transcendentals over C are constants

Proved

OAI.PiExponent.FormalInterpolation.exists_eq_algebraMap_of_not_transcendental

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

algebraic-geometryformal-interpolation

If $E$ is a field extension of the algebraically closed field $\mathbb{C}$ and $f\in E$ is not transcendental over $\mathbb{C}$ , then $f$ lies in the image of the structure map $\mathbb{C}\to E$ .

Preamble

import Mathlib.Data.Complex.Basic
import Mathlib.FieldTheory.IsAlgClosed.Basic
import Mathlib.RingTheory.Algebraic.Basic

Formal statement

theorem OAI.PiExponent.FormalInterpolation.exists_eq_algebraMap_of_not_transcendental
    {E : Type} [Field E] [Algebra Complex E]
    (f : E) (hf : ¬Transcendental Complex f) :
    ∃ b : Complex, algebraMap Complex E b = f := by sorry

Source

Mission d7ce6393

View graph