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},
}
|