iteratedDeriv_odd_sinh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

English

The (2n+1)-th derivative of sinh equals cosh.

Русский

(2n+1)-я производная от sinh равна cosh.

LaTeX

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

Lean4

theorem iteratedDeriv_odd_sinh (n : ℕ) : iteratedDeriv (2 * n + 1) sinh = cosh := by simp

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

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

Разделы

Аффилиация

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