iteratedDeriv_odd_cosh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

English

For every natural number n, the (2n+1)-st derivative of cosh is sinh.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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