Euler's Formula

Stream: Is there code for X?

[Mark Gerads]

I did not find this with library_search. Help would be appreciated, and this probably belongs in mathlib somewhere.

import all

open complex real

lemma EulersFormula : exp (I * ↑real.pi) = -1 :=
begin
  sorry,
end

[Hanting Zhang]

I don't think it exists, but you are very close after docs#complex.exp_mul_I and docs#complex, docs#complex.sin_pi

[Adam Topaz]

import data.complex.exponential
import analysis.special_functions.trigonometric.basic

example : complex.exp (↑real.pi * complex.I) = -1 := by simp

[Adam Topaz]

Now you can copy that code, and replace simp with squeeze_simp to see what lemmas were used :)