cosh_add

Mathlib.Analysis.Complex.Trigonometric

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

English

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

Русский

Для любых вещественных x,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

nonrec theorem cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y := by rw [← ofReal_inj]; simp [cosh_add]

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

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

Разделы

Аффилиация

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