ofReal_cosh

Mathlib.Analysis.Complex.Trigonometric

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

English

The complex cosh of a real input equals the real cosh: (Real.cosh x : ℂ) = cosh x.

Русский

Комплексный косh от вещественного аргумента соответствует вещественному cosh: (Real.cosh x : ℂ) = cosh x.

LaTeX

$$$(\operatorname{Real.cosh} x : \mathbb{C}) = \cosh x$$$

Lean4

@[simp, norm_cast]
theorem ofReal_cosh (x : ℝ) : (Real.cosh x : ℂ) = cosh x :=
  ofReal_cosh_ofReal_re _

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

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

Разделы

Аффилиация

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