3 Hermite–Lindemann and Lindemann–Weierstrass

The Lean proof of Lindemann–Weierstrass is ported from Mathlib pull request #28013 by Yuyang Zhao, which is not merged; it depends on Mathlib alone. Hermite–Lindemann is derived from it, in two equivalent forms. The four exponentials development uses Hermite–Lindemann to make one generator of a field transcendental.

Theorem 3.1 Lindemann–Weierstrass

✓

Let \(\alpha _1,\dots ,\alpha _n\) be pairwise distinct algebraic numbers. Then \(e^{\alpha _1},\dots ,e^{\alpha _n}\) are linearly independent over \(\overline{\mathbb {Q}}\): if \(\beta _1,\dots ,\beta _n\in \overline{\mathbb {Q}}\) are not all zero, then \(\sum _i\beta _ie^{\alpha _i}\neq 0\).
If algebraic numbers \(\alpha _1,\dots ,\alpha _n\) are linearly independent over \(\mathbb {Q}\), then \(e^{\alpha _1},\dots ,e^{\alpha _n}\) are algebraically independent over \(\overline{\mathbb {Q}}\).

(The Lean statements take families indexed by any type; in (b) they ask for linear independence over \(\mathbb {N}\), which for a family in a \(\mathbb {Q}\)-vector space is the same.)

Source: Lindemann [ Lin1882 ] , Weierstrass [ Wei1885 ] ; see [ Bak75 , Theorem 1.4 ] .

Proof ▶

(a) is the proof of the Mathlib pull request. (b) applies (a) to the numbers \(\sum _ie_i\alpha _i\), \(e\in \mathbb {N}^{n}\), which are pairwise distinct.

Theorem 3.2 Hermite–Lindemann

✓

If \(a\) is a non-zero algebraic number, then \(e^{a}\) is transcendental.

Source: Hermite [ Her1873 ] for \(a=1\), Lindemann [ Lin1882 ] in general; see [ Bak75 , Theorem 1.4 ] .

Proof ▶

Apply Theorem 3.1(a) to \(\alpha =(a,0)\) and \(\beta =(1,-e^{a})\).

Theorem 3.3 Hermite–Lindemann, logarithmic form

✓

Let \(u\in \mathbb {C}\), \(u\neq 0\), with \(e^{u}\) algebraic. Then \(u\) is transcendental.

Source: Hermite [ Her1873 ] , Lindemann [ Lin1882 ] ; see [ Bak75 , Theorem 1.4 ] .

Proof ▶

Apply Theorem 3.1(a) to \(\alpha =(u,0)\) and \(\beta =(1,-e^{u})\). This is the form the rest of the library uses; Theorem 3.2 is its contrapositive. (The accepted Prove2Me proof derives it from Theorem 3.2; the library’s proof, shown here, does not.)