cosh_neg

Mathlib.Analysis.Complex.Trigonometric

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

English

Cosh is an even function: cosh(-x) = cosh(x).

Русский

cosh — четная функция: cosh(-x) = cosh(x).

LaTeX

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

Lean4

@[simp]
theorem cosh_neg : cosh (-x) = cosh x := by simp [add_comm, cosh, exp_neg]

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

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

Разделы

Аффилиация

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