sin_eq_tsum — Mathlib

English

The complex sine function can be written as sin z = ∑_{n=0}^∞ (-1)^n z^{2n+1}/(2n+1)!, i.e. the standard sine-series.

Русский

Комплексный синус записывается как 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 : ℕ, (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)! :=
  (Complex.hasSum_sin z).tsum_eq.symm

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