lemma exp_pi_mul_I_half : exp (↑real.pi * I / 2) = I :=

Stream: Is there code for X?

[Mark Gerads]

I need to simplify this in a proof

lemma exp_pi_mul_I_half : exp (↑real.pi * I / 2) = I :=

Currently attempting proof.

[Kevin Buzzard]

import analysis.special_functions.trigonometric.basic

open complex

noncomputable abbreviation pi := real.pi

lemma exp_pi_mul_I_half : exp (↑pi * I / 2) = I :=
begin
  -- would rather the /2 is real
  rw (show (pi : ℂ) * I / 2 = (pi / 2 : ℝ) * I, by {simp, ring, } ),
  -- now apply Euler, which was bound to be there in some form
  rw exp_mul_I,
  -- now hope simplifier knows all the facts about cos(pi/2) etc.
  simp,
  -- it does!
end