Email Gateway (Aug 22 2022 at 14:57): Email Gateway (Aug 22 2022 at 14:57):From: Gerwin.Klein@data61.csiro.au
A new AFP entry is available:
The Transcendence of e
Manuel Eberl
This work contains a proof that Euler's number e is transcendental. The proof follows the standard approach of assuming that e is algebraic and then using a specific integer polynomial to derive two inconsistent bounds, leading to a contradiction.
This kind of approach can be found in many different sources; this formalisation mostly follows a PlanetMath article by Roger Lipsett.
https://www.isa-afp.org/entries/E_Transcendental.shtml
Enjoy!
Gerwin
Last updated: Apr 25 2024 at 12:23 UTC