ofReal_sinh_ofReal_re

Mathlib.Analysis.Complex.Trigonometric

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

English

Let x be real. The real part of sinh(Complex.ofReal x) equals sinh x.

Русский

Пусть x — вещественное. Действительная часть sinh(Complex.ofReal x) равна sinh x.

LaTeX

$$$\operatorname{Re}(\sinh(\operatorname{ofReal} x)) = \sinh x$$$

Lean4

@[simp]
theorem ofReal_sinh_ofReal_re (x : ℝ) : ((sinh x).re : ℂ) = sinh x :=
  conj_eq_iff_re.1 <| by rw [← sinh_conj, conj_ofReal]

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

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

Разделы

Аффилиация

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