### 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\}$

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Hermite_Lindemann

- Algebraic_Integer_Divisibility
- More_Polynomial_HLW
- More_Min_Int_Poly
- Complex_Lexorder
- More_Multivariate_Polynomial_HLW
- More_Algebraic_Numbers_HLW
- Misc_HLW
- Hermite_Lindemann

### Depends on

- Algebraic Numbers in Isabelle/HOL
- The Transcendence of π
- Power Sum Polynomials

### Used by

- Factorization of Polynomials with Algebraic Coefficients

### Auto-related entries

- Factorization of Polynomials with Algebraic Coefficients
- The Transcendence of Certain Infinite Series

## Cite

×

Hermite_Lindemann-AFP

    @article{Hermite_Lindemann-AFP,
      author  = {Manuel Eberl},
      title   = {The Hermite–Lindemann–Weierstraß Transcendence Theorem},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Hermite_Lindemann.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Mar 12, 2021 : Isabelle2021