hasSum_cosh — Mathlib

English

The complex cosh has the Maclaurin series cosh z = ∑_{n=0}^∞ z^{2n}/(2n)!, i.e. the even-power cosine hyperbolic series.

Русский

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

LaTeX

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

Lean4

/-- The power series expansion of `Complex.cosh`. -/
theorem hasSum_cosh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n) / ↑(2 * n)!) (cosh z) := by
  simpa [mul_assoc, cos_mul_I] using hasSum_cos' (z * I)

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