English
An alternate but equivalent form of the complex sine expansion is sin z = ∑_{n=0}^∞ (z i)^{2n+1}/((2n+1)! i), which simplifies to the standard sum.
Русский
Альтернативная, эквивалентная форма разложения синуса комплексного аргумента: sin z = ∑_{n=0}^∞ (z i)^{2n+1}/((2n+1)! i), что в итоге даёт стандартный ряд.
LaTeX
$$$\\sin z = \\sum_{n=0}^{\\infty} \\frac{(z i)^{2n+1}}{(2n+1)!\, i}$$$
Lean4
/-- The power series expansion of `Complex.sin`. -/
theorem hasSum_sin (z : ℂ) : HasSum (fun n : ℕ => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (Complex.sin z) :=
by
convert Complex.hasSum_sin' z using 1
simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
