The Lindemann–Weierstrass theorem

This file proves the Lindemann–Weierstrass theorem for algebraic numbers, in the two classical forms. Here the field of algebraic numbers is integralClosure ℚ ℂ.

• linearIndependent_exp: the exponentials of pairwise distinct algebraic numbers are linearly independent over the algebraic numbers (Baker's form of the theorem).
• algebraicIndependent_exp: the exponentials of ℚ-linearly independent algebraic numbers are algebraically independent over the algebraic numbers. The hypothesis is stated as linear independence over ℕ, which for the ℚ-vector space of algebraic numbers is equivalent to linear independence over ℚ. It says exactly that distinct monomials ∏ (exp uᵢ) ^ mᵢ = exp (∑ mᵢ uᵢ) have distinct exponents, so that the first form applies.

Both are deduced from the injectivity of exponential evaluation over a number field that is Galois over ℚ (LindemannWeierstrass.expEval_injective), in the form of linear independence of exponentials (LindemannWeierstrass.linearIndependent_exp_algebraMap): the finitely many exponents and coefficients of a given linear relation lie in such a field (exists_isGalois_superset_of_isAlgClosed).

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 4, §4.2, Theorem 4.8, its deduction from Theorem 4.11, and Corollary 4.10.
• Y. Zhao, formalization of the Lindemann–Weierstrass theorem in Lean, Basic.lean, theorems linearIndependent_exp and algebraicIndependent_exp, whose statements are followed here.

theorem TauCeti.linearIndependent_exp {ι : Type u_1} (u : ι → ↥(integralClosure ℚ ℂ)) (u_inj : Function.Injective u) : LinearIndependent ↥(integralClosure ℚ ℂ) fun (i : ι) => Complex.exp ↑(u i)

The Lindemann–Weierstrass theorem, in Baker's form. The exponentials of pairwise distinct algebraic numbers are linearly independent over the field integralClosure ℚ ℂ of algebraic numbers.

theorem TauCeti.algebraicIndependent_exp {ι : Type u_1} (u : ι → ↥(integralClosure ℚ ℂ)) (hu : LinearIndependent ℕ u) : AlgebraicIndependent ↥(integralClosure ℚ ℂ) fun (i : ι) => Complex.exp ↑(u i)

The Lindemann–Weierstrass theorem, algebraic independence form. If the algebraic numbers u i are linearly independent over ℕ (equivalently, over ℚ), then their exponentials are algebraically independent over the field integralClosure ℚ ℂ of algebraic numbers.