| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
The Transcendence of π
| Title: | The Transcendence of π |
| Author: | Manuel Eberl |
| Submission date: | 2018-09-28 |
| Abstract: |
This entry shows the transcendence of π based on the classic proof using the fundamental theorem of symmetric polynomials first given by von Lindemann in 1882, but the formalisation mostly follows the version by Niven. The proof reuses much of the machinery developed in the AFP entry on the transcendence of e. |
| BibTeX: |
@article{Pi_Transcendental-AFP,
author = {Manuel Eberl},
title = {The Transcendence of π},
journal = {Archive of Formal Proofs},
month = sep,
year = 2018,
note = {\url{https://isa-afp.org/entries/Pi_Transcendental.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | E_Transcendental, Symmetric_Polynomials |
| Used by: | Hermite_Lindemann |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |