Hermite--Lindemann theorem

Proved

transcendental_exp

by lisamegawatts · Sep 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

lindemann-weierstrass-lean430-backportnumber-theorytranscendence

For every nonzero algebraic complex number $a$ ,

e^a\text{ is transcendental over }\mathbb Z.

Equivalently, no nonzero polynomial with integer coefficients vanishes at $e^a$ .

Preamble

import Mathlib.Analysis.SpecialFunctions.Complex.Log
import Mathlib.RingTheory.Algebraic.Defs
import Mathlib.RingTheory.AlgebraicIndependent.Defs
import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Analysis.Complex.IsIntegral
import Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

open scoped Nat AddMonoidAlgebra
open Complex Finset Polynomial

variable {ι : Type*}

Formal statement

theorem transcendental_exp {a : ℂ} (a0 : a ≠ 0) (ha : IsAlgebraic ℤ a) :
    Transcendental ℤ (exp a) := by sorry

Source

Yuyang Zhao, mathlib4 PR #28013, Lindemann--Weierstrass theorem, c5ea-compatible snapshot 5abb7c68488b527e4d7ecf5d7bbe085db8d2a388; https://github.com/leanprover-community/mathlib4/pull/28013. Mathematical source: Nathan Jacobson, Basic Algebra I, 2nd ed., §4.12, Theorem 4.22.

Human review

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

View graph