exp_im

Mathlib.Analysis.Complex.Trigonometric

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

English

For any complex x, Im(exp x) = exp(Re x) sin(Im x).

Русский

Для любого комплексного x: Im(exp x) = exp(Re x) sin(Im x).

LaTeX

$$$\\forall x \\in \\mathbb{C},\\; \\Im(e^{x}) = e^{\\Re x} \\sin(\\Im x)$$$

Lean4

theorem exp_im : (exp x).im = Real.exp x.re * Real.sin x.im :=
  by
  rw [exp_eq_exp_re_mul_sin_add_cos]
  simp [exp_ofReal_re, sin_ofReal_re]

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

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

Разделы

Аффилиация

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