Lindemann--Weierstrass exponential linear independence

Proved

linearIndependent_exp

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

lindemann-weierstrass-lean430-backportnumber-theorytranscendence

Let $u_i$ be an injective family of algebraic complex numbers. Then the family of exponentials is linearly independent over the algebraic closure of $\mathbb Q$ :

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

The index type may be infinite; linear independence reduces every relation to a finite support.

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 linearIndependent_exp (u : ι → integralClosure ℚ ℂ) (u_inj : u.Injective) :
    LinearIndependent (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