cosh_sub

Mathlib.Analysis.Complex.Trigonometric

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

English

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

Русский

cosh(x - y) = cosh x cosh y - sinh x sinh y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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