sinh_sub

Mathlib.Analysis.Complex.Trigonometric

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

English

Sinh of a difference: sinh(x - y) = sinh x cosh y - cosh x sinh y.

Русский

Sinh разности: 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