sinh_add_cosh

Mathlib.Analysis.Complex.Trigonometric

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

English

Sinh x plus cosh x equals exp x.

Русский

Sinh x плюс cosh x равно exp x.

LaTeX

$$$\sinh x + \cosh x = \exp x$$$

Lean4

@[simp]
theorem sinh_add_cosh : sinh x + cosh x = exp x := by rw [add_comm, cosh_add_sinh]

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

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

Разделы

Аффилиация

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