Eulers_Number_is_Irrational

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

euler-s-numberirrationality-proofsproofwiki

Eulers number e is irrational

Preamble

import Mathlib.NumberTheory.Real.Irrational
import Mathlib.Analysis.SpecialFunctions.ExpDeriv

Formal statement

theorem Eulers_Number_is_Irrational : Irrational (Real.exp 1) := by sorry