hasDerivAt_sinh

Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

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

← MathLib Explorer

English

The derivative of sinh is cosh: d/dz sinh z = cosh z for all z.

Русский

Производная sinh равна cosh: d/dz sinh z = cosh z для всех z.

LaTeX

$$$\dfrac{d}{dz}\sinh z = \cosh z \quad\text{for all } z \in \mathbb{C}$$$

Lean4

/-- The complex hyperbolic sine function is everywhere differentiable, with the derivative
`cosh x`. -/
theorem hasDerivAt_sinh (x : ℂ) : HasDerivAt sinh (cosh x) x :=
  (hasStrictDerivAt_sinh x).hasDerivAt

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

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

Разделы

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

Аффилиация

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