 # The Hermite–Lindemann–Weierstraß Transcendence Theorem

 Title: The Hermite–Lindemann–Weierstraß Transcendence Theorem Author: Manuel Eberl Submission date: 2021-03-03 Abstract: 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, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,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, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \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\}$ BibTeX: @article{Hermite_Lindemann-AFP, author = {Manuel Eberl}, title = {The Hermite–Lindemann–Weierstraß Transcendence Theorem}, journal = {Archive of Formal Proofs}, month = mar, year = 2021, note = {\url{https://isa-afp.org/entries/Hermite_Lindemann.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Algebraic_Numbers, Pi_Transcendental, Power_Sum_Polynomials