tanh_eq_sinh_div_cosh

Mathlib.Analysis.Complex.Trigonometric

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

English

For all real x, tanh x = sinh x / cosh x.

Русский

Для всех x: tanh x = sinh x / cosh x.

LaTeX

$$$\\tanh x = \\frac{\\sinh x}{\\cosh x}$$$

Lean4

nonrec theorem tanh_eq_sinh_div_cosh : tanh x = sinh x / cosh x :=
  ofReal_inj.1 <| by simp [tanh_eq_sinh_div_cosh]

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

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

Разделы

Аффилиация

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