Theorem: exp_of_im (Ray/Hartogs/FubiniBall.lean)

State before:
t : ℝ
⊢ (↑t * I).exp = ↑t.cos + ↑t.sin * I
Tactic:
simp [Complex.ext_iff, Complex.cos_ofReal_re, Complex.sin_ofReal_re]
State after:
no goals