Prove2Me

Integral orbit-sum reduction for exponential relations

Proved
linearIndependent_exp_aux

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

lindemann-weierstrass-lean430-backportnumber-theorytranscendence

Let SS be an algebraically closed field over Q\mathbb Q, and let ϕ\phi be a multiplicative character on its additive group. Given pairwise distinct integral exponents uiu_i and a nonzero integral coefficient family viv_i satisfying ∑iviϕ(ui)=0\sum_i v_i\phi(u_i)=0, there are an integer w≠0w\ne0, integer polynomials pjp_j with nonzero constant terms, and integer weights wj′w'_j such that

w+∑jwj′∑r∈Roots⁡(pj)ϕ(r)=0.w+\sum_j w'_j\sum_{r\in\operatorname{Roots}(p_j)}\phi(r)=0.

This is the Galois-symmetrized algebraic reduction that converts an arbitrary algebraic relation into an integer orbit-sum relation.

Preamble
import Mathlib.FieldTheory.IsAlgClosed.Basic

open scoped Nat AddMonoidAlgebra
open Complex Finset Polynomial

variable {ι : Type*} [Fintype ι]
Formal statement
theorem linearIndependent_exp_aux {S : Type*}
    [Field S] [Algebra ℚ S] [IsAlgClosed S]
    (phi : Multiplicative S →* S)
    (u : ι → S) (hu : ∀ i, IsIntegral ℚ (u i))
    (u_inj : Function.Injective u) (v : ι → S) (hv : ∀ i, IsIntegral ℚ (v i)) (v0 : v ≠ 0)
    (h : ∑ i, v i * phi (.ofAdd <| u i) = 0) :
    ∃ (w : ℤ) (_w0 : w ≠ 0) (n : ℕ) (p : Fin n → ℤ[X]) (_p0 : ∀ j, (p j).eval 0 ≠ 0)
      (w' : Fin n → ℤ),
        w + ∑ j, w' j • (((p j).aroots S).map (phi <| .ofAdd ·)).sum = 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