sinh_eq

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

sinh x = (exp x − exp(−x)) / 2

Русский

sinh x = (exp x − exp(−x)) / 2

LaTeX

$$\$\\sinh x = \\frac{e^x - e^{-x}}{2}\\$$$

Lean4

/-- The definition of `sinh` in terms of `exp`. -/
nonrec theorem sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 :=
  ofReal_injective <| by simp [Complex.sinh]

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

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

Разделы

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

Аффилиация

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