ofReal_sinh

Mathlib.Analysis.Complex.Trigonometric

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

English

For real x, the complex value (Real.sinh x) equals sinh(Complex.ofReal x).

Русский

Для вещественного x равенство: (Real.sinh x) в комплексном виде равно sinh(Complex.ofReal x).

LaTeX

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

Lean4

@[simp, norm_cast]
theorem ofReal_sinh (x : ℝ) : (Real.sinh x : ℂ) = sinh x :=
  ofReal_sinh_ofReal_re _

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

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

Разделы

Аффилиация

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