exp_re

Mathlib.Analysis.Complex.Trigonometric

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

English

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

Русский

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

LaTeX

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

Lean4

theorem exp_re : (exp x).re = Real.exp x.re * Real.cos x.im :=
  by
  rw [exp_eq_exp_re_mul_sin_add_cos]
  simp [exp_ofReal_re, cos_ofReal_re]

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

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

Разделы

Аффилиация

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