case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (cos z)
convert Complex.hasSum_cos' z using 1
no goals
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!
simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]