hasSum_sinh — Mathlib

English

For real x, Real.sin x has the Maclaurin series sin x = ∑ (-1)^n x^{2n+1}/(2n+1)!.

Русский

Для действительного x синус имеет ряд Маклорена: sin x = ∑ (-1)^n x^{2n+1}/(2n+1)!.

LaTeX

$$$\\sin x = \\sum_{n=0}^{\\infty} (-1)^n \\frac{x^{2n+1}}{(2n+1)!}$$$

Lean4

/-- The power series expansion of `Real.sinh`. -/
theorem hasSum_sinh (r : ℝ) : HasSum (fun n ↦ r ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh r) :=
  mod_cast Complex.hasSum_sinh r

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