sinh_eq_tsum — Mathlib

English

One has the identities sinh z = ∑ z^{2n+1}/(2n+1)!, cosh z = ∑ z^{2n}/(2n)!, and cosh z = (e^z + e^{-z})/2, sinh z = (e^z - e^{-z})/2 when viewed through their series.

Русский

Существуют ряды для sinh и cosh: sinh z = ∑ z^{2n+1}/(2n+1)!, cosh z = ∑ z^{2n}/(2n)!, а также связи через экспоненты.

LaTeX

$$$\\sinh z = \\sum_{n=0}^{\\infty} \\frac{z^{2n+1}}{(2n+1)!}, \\cosh z = \\sum_{n=0}^{\\infty} \\frac{z^{2n}}{(2n)!}$$$

Lean4

theorem sinh_eq_tsum (z : ℂ) : sinh z = ∑' n, z ^ (2 * n + 1) / ↑(2 * n + 1)! :=
  z.hasSum_sinh.tsum_eq.symm

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