sin_add_sin

Mathlib.Analysis.Complex.Trigonometric

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

English

For all complex x,y, sin x + sin y = 2 sin((x + y)/2) cos((x − y)/2).

Русский

Для любых комплексных x и y верно: sin x + sin y = 2 sin((x + y)/2) cos((x − y)/2).

LaTeX

$$$ \sin x + \sin y = 2 \sin\left(\frac{x + y}{2}\right) \cos\left(\frac{x - y}{2}\right).$$$

Lean4

theorem sin_add_sin : sin x + sin y = 2 * sin ((x + y) / 2) * cos ((x - y) / 2) := by simpa using sin_sub_sin x (-y)

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

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

Разделы

Аффилиация

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