cosh_eq_tsum — Mathlib

English

The hyperbolic cosine cosh and ordinary cosine cos relate to their series: cosh z = ∑ z^{2n}/(2n)!, cos z = ∑ (-1)^n z^{2n}/(2n)!.

Русский

Связь косинуса и гиперболического косинуса с рядами: cos z = ∑ (-1)^n z^{2n}/(2n)!, cosh z = ∑ z^{2n}/(2n)!.

LaTeX

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

Lean4

theorem cosh_eq_tsum (z : ℂ) : cosh z = ∑' n, z ^ (2 * n) / ↑(2 * n)! :=
  z.hasSum_cosh.tsum_eq.symm

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