exp_eq_exp_re_mul_sin_add_cos — Mathlib

English

For any complex x, exp x = exp(re(x)) (cos im(x) + i sin im(x)).

Русский

Для любого комплексного x: exp x = exp(реальные часть) (cos мнимая часть + i sin мнимая часть).

LaTeX

$$$\\forall x \\in \\mathbb{C},\\; e^{x} = e^{\\operatorname{Re} x} \\left(\\cos(\\operatorname{Im} x) + i \\sin(\\operatorname{Im} x)\\right)$$$

Lean4

theorem exp_eq_exp_re_mul_sin_add_cos : exp x = exp x.re * (cos x.im + sin x.im * I) := by
  rw [← exp_add_mul_I, re_add_im]

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