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