iteratedDeriv_even_sinh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

URI: https://scilib.ai/kg/mathlib#Complex.iteratedDeriv_even_sinh

← MathLib Explorer

English

For every natural number n, the 2n-th derivative of sinh coincides with sinh itself.

Русский

Пусть n натуральное. 2n-я производная от sinh совпадает с sinh.

LaTeX

$$$\\\\frac{d^{2n}}{dx^{2n}} \\\\sinh x = \\\\sinh x$$$

Lean4

@[simp]
theorem iteratedDeriv_even_sinh (n : ℕ) : iteratedDeriv (2 * n) sinh = sinh := by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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