cos_sub_sin_I

Mathlib.Analysis.Complex.Trigonometric

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

English

Equivalently, cos z − i sin z = exp(− i z) for all complex z.

Русский

Соответствующая форма: cos z − i sin z = e^{− i z} для всех комплексных z.

LaTeX

$$$\\forall z \\in \\mathbb{C},\\; \\cos z - i \\sin z = e^{-i z}$$$

Lean4

theorem cos_sub_sin_I : cos x - sin x * I = exp (-x * I) := by rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]

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

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

Разделы

Аффилиация

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