contDiff_cos — Mathlib

English

cos is infinitely differentiable; in particular, cos x has the Maclaurin series cos x = sum_{k=0}^\infty (-1)^k x^{2k}/(2k)!.

Русский

cos бесконечно дифференцируема; в частности, Маклоренова серия cos x = \\sum_{k=0}^\infty (-1)^k x^{2k}/(2k)!.

LaTeX

$$$\\cos x = \\displaystyle \\sum_{k=0}^{\\infty} (-1)^k \\frac{x^{2k}}{(2k)!}$$$

Lean4

@[fun_prop]
theorem contDiff_cos {n} : ContDiff ℝ n cos :=
  Complex.contDiff_cos.real_of_complex

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