hasSum_sin — Mathlib

English

For every z in ℂ, the complex sine has a series representation sin z = ∑_{n=0}^∞ (-1)^n z^{2n+1}/(2n+1)!, i.e. the Maclaurin expansion.

Русский

Для каждого z ∈ ℂ синус имеет ряд Маклорена: 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

/-- The power series expansion of `Real.sin`. -/
theorem hasSum_sin (r : ℝ) : HasSum (fun n : ℕ => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1)!) (Real.sin r) :=
  mod_cast Complex.hasSum_sin r

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