exp_mul_I

Mathlib.Analysis.Complex.Trigonometric

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

English

The complex exponential with imaginary argument satisfies exp(i x) = cos x + i sin x.

Русский

Комплексная экспонента с мнимым аргументом удовлетворяет exp(i x) = cos x + i sin x.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; e^{i x} = \\cos x + i \\sin x$$$

Lean4

theorem exp_mul_I : exp (x * I) = cos x + sin x * I :=
  (cos_add_sin_I _).symm

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

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

Разделы

Аффилиация

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