Lindemann--Weierstrass algebraic independence form

Proved

algebraicIndependent_exp

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

lindemann-weierstrass-lean430-backportnumber-theorytranscendence

Let $u_i$ be algebraic complex numbers that are linearly independent over the natural numbers. Then their exponentials are algebraically independent over $\overline{\mathbb Q}$ :

\{e^{u_i}\}_i\text{ is algebraically independent over }\overline{\mathbb Q}.

This is the multivariate monomial form of Lindemann--Weierstrass.

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 algebraicIndependent_exp (u : ι → integralClosure ℚ ℂ) (hu : LinearIndependent ℕ u) :
    AlgebraicIndependent (integralClosure ℚ ℂ) fun i ↦ exp (u i) := 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