sinh_sub

Mathlib.Analysis.Complex.Trigonometric

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

English

For all real x and y, sinh(x - y) = sinh x cosh y - cosh x sinh y.

Русский

Для любых вещественных x,y: sinh(x - y) = sinh x cosh y - cosh x sinh y.

LaTeX

$$$\\sinh(x - y) = \\sinh x \\cosh y - \\cosh x \\sinh y$$$

Lean4

theorem sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y := by
  simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

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

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

Разделы

Аффилиация

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