cos_eq_tsum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem cos_eq_tsum (r : ℝ) : Real.cos r = ∑' n : ℕ, (-1) ^ n * r ^ (2 * n) / ↑(2 * n)! :=
  (Real.hasSum_cos r).tsum_eq.symm

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