contDiff_sin

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Real.contDiff_sin

English

For every natural number n, the nth derivative of sin is sin(x + nπ/2).

Русский

Для каждого натурального числа n n-я производная синуса равна sin(x + nπ/2).

LaTeX

$$$\\displaystyle \\frac{d^{n}}{dx^{n}} \\sin x = \\sin\\left( x + \\frac{\\pi}{2} n \\right) \\quad (n \\in \\mathbb{N})$$$

Lean4

@[fun_prop]
theorem contDiff_sin {n} : ContDiff ℝ n sin :=
  Complex.contDiff_sin.real_of_complex

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru