hasSum_cos — Mathlib

English

Cos z equals the complex power-series cos z = ∑_{n=0}^∞ (-1)^n z^{2n}/(2n)!, i.e. the standard cosine expansion.

Русский

Косинус комплексного аргумента через ряд: cos z = ∑_{n=0}^∞ (-1)^n z^{2n}/(2n)!, стандартное разложение косинуса.

LaTeX

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

Lean4

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

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