Finite Lindemann--Weierstrass linear relation

Proved

linearIndependent_exp_finite

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

lindemann-weierstrass-lean430-backportnumber-theorytranscendence

For a finite family of pairwise distinct algebraic complex numbers $u_i$ and algebraic coefficients $v_i$ ,

\sum_i v_i e^{u_i}=0\quad\Longrightarrow\quad v_i=0\text{ for every }i.

This finite form is the analytic-algebraic heart of the Lindemann--Weierstrass theorem.

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_finite [Fintype ι] (u : ι → ℂ) (hu : ∀ i, IsIntegral ℚ (u i))
    (u_inj : Function.Injective u) (v : ι → ℂ) (hv : ∀ i, IsIntegral ℚ (v i))
    (h : ∑ i, v i * exp (u i) = 0) : v = 0 := 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