hasSum_sinh — Mathlib

English

The complex sinh has the Maclaurin series sinh z = ∑_{n=0}^∞ z^{2n+1}/(2n+1)!, i.e. the odd-power sinh-series.

Русский

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

LaTeX

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

Lean4

/-- The power series expansion of `Complex.sinh`. -/
theorem hasSum_sinh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh z) := by
  simpa [mul_assoc, sin_mul_I, neg_pow z, pow_add, pow_mul, neg_mul, neg_div] using (hasSum_sin' (z * I)).mul_right (-I)

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