Eulers_Identity

Proved

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

complex-analysiseuler-s-numberpiproofwiki

$e^{i \pi} + 1 = 0$

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Circle

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Circle

theorem Eulers_Identity : Complex.exp (↑Real.pi * Complex.I) + 1 = 0 := by sorry

Source

https://proofwiki.org/wiki/Euler's_Identity

View graph