Abstract
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.