exp_add_mul_I

Mathlib.Analysis.Complex.Trigonometric

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

English

For complex x, y, exp(x + y i) = exp(x) (cos y + i sin y).

Русский

Для комплексных x, y: exp(x + y i) = exp(x) (cos y + i sin y).

LaTeX

$$$\\forall x,y \\in \\mathbb{C},\\; e^{x + y i} = e^{x}\\bigl(\\cos y + i \\sin y\\bigr)$$$

Lean4

theorem exp_add_mul_I : exp (x + y * I) = exp x * (cos y + sin y * I) := by rw [exp_add, exp_mul_I]

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

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

Разделы

Аффилиация

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