hasSum_cosh — Mathlib

English

For real numbers r, Real.cos r has the same Maclaurin expansion: cos r = ∑_{n=0}^∞ (-1)^n r^{2n}/(2n)!.

Русский

Для действительных r косинус имеет разложение: cos r = ∑_{n=0}^∞ (-1)^n r^{2n}/(2n)!.

LaTeX

$$$\\cos r = \\sum_{n=0}^{\\infty} (-1)^n \\frac{r^{2n}}{(2n)!}$$$

Lean4

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

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