The Hermite–Lindemann–Weierstraß Transcendence Theorem

This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.

The theorem states that if ${\alpha }_1,\dots ,{\alpha }_n\in \mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{{\alpha }_1},\dots ,e^{{\alpha }_n}$ are algebraically independent over $\mathbb{Q}$.

Like the previous formalisation in Coq by Bernard, I proceeded by formalising Baker's version of the theorem and proof and then deriving the original one from that. Baker's version states that for any algebraic numbers ${\beta }_1,\dots ,{\beta }_n\in \mathbb{C}$ and distinct algebraic numbers ${\alpha }_i,\dots ,{\alpha }_n\in \mathbb{C}$, we have ${\beta }_1{e}^{{\alpha }_1}+\dots +{\beta }_n{e}^{{\alpha }_n}=0$ if and only if all the ${\beta }_i$ are zero.

This has a number of direct corollaries, e.g.:

• $e$ and $\pi$ are transcendental
• $e^z$, $\sin z$, $\tan z$, etc. are transcendental for algebraic $z\in \mathbb{C}\setminus \{0\}$
• $\ln z$ is transcendental for algebraic $z\in \mathbb{C}\setminus \{0,1\}$