exp_sub_cosh

Mathlib.Analysis.Complex.Trigonometric

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

English

exp x minus cosh x equals sinh x.

Русский

exp x минус cosh x равно sinh x.

LaTeX

$$$\exp x - \cosh x = \sinh x$$$

Lean4

@[simp]
theorem exp_sub_cosh : exp x - cosh x = sinh x :=
  sub_eq_iff_eq_add.2 (sinh_add_cosh x).symm

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

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

Разделы

Аффилиация

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