sin_eq_tsum' — Mathlib

English

The complex sine function equals the standard sine series: sin z = ∑_{n=0}^∞ (-1)^n z^{2n+1}/(2n+1)!.

Русский

Функция синуса комплексного аргумента равна стандартному ряду синуса: sin z = ∑_{n=0}^∞ (-1)^n z^{2n+1}/(2n+1)!.

LaTeX

$$$\\sin z = \\sum_{n=0}^{\\infty} (-1)^n \\frac{z^{2n+1}}{(2n+1)!}$$$

Lean4

theorem sin_eq_tsum' (z : ℂ) : Complex.sin z = ∑' n : ℕ, (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1)! / Complex.I :=
  (Complex.hasSum_sin' z).tsum_eq.symm

Похожие утверждения