cosh_abs

Mathlib.Analysis.Complex.Trigonometric

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

English

cosh(|x|) = cosh(x) for all x.

Русский

cosh(|x|) = cosh(x) для всех x.

LaTeX

$$$\\cosh(\\lvert x \\rvert) = \\cosh x$$$

Lean4

@[simp]
theorem cosh_abs : cosh |x| = cosh x := by cases le_total x 0 <;> simp [*, abs_of_nonneg, abs_of_nonpos]

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

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

Разделы

Аффилиация

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