hasSum_cos — Mathlib

English

For every complex z, cos z equals its Maclaurin series cos z = ∑_{n=0}^∞ (-1)^n z^{2n}/(2n)!.

Русский

Для любого комплексного числа z косинус равен своему степенному разложению: 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 `Complex.cos`. -/
theorem hasSum_cos (z : ℂ) : HasSum (fun n : ℕ => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (Complex.cos z) :=
  by
  convert Complex.hasSum_cos' z using 1
  simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]

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