two_sin

Mathlib.Analysis.Complex.Trigonometric

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

English

2 sin x = i (e^{-i x} - e^{i x}).

Русский

2 sin x = i (e^{-i x} - e^{i x}).

LaTeX

$$$2 \\sin x = i \\left(e^{-i x} - e^{i x}\\right)$$$

Lean4

theorem two_sin : 2 * sin x = (exp (-x * I) - exp (x * I)) * I :=
  mul_div_cancel₀ _ two_ne_zero

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

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

Разделы

Аффилиация

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