Prove2Me

Eulers_Formula

Proved

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

euler-s-formulaexponential-functionproofwikitrigonometric-functions

Euler's formula: e^(iz) = cos(z) + i*sin(z)

Preamble
import Mathlib.Analysis.SpecialFunctions.Complex.Circle
import Mathlib.Tactic
Formal statement
theorem Eulers_Formula (z : ℝ) : Complex.exp (Complex.I * z) = Complex.ofReal (Real.cos z) + Complex.I * Complex.ofReal (Real.sin z) := by sorry
Source
https://proofwiki.org/wiki/Euler's_Formula

View graph