sin_add

Mathlib.Analysis.Complex.Trigonometric

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

← MathLib Explorer

English

sin(x + y) = sin x cos y + cos x sin y.

Русский

sin(x + y) = sin x cos y + cos x sin y.

LaTeX

$$$\\sin(x + y) = \\sin x \\cos y + \\cos x \\sin y$$$

Lean4

theorem sin_add : sin (x + y) = sin x * cos y + cos x * sin y := by
  rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, add_mul, add_mul, mul_right_comm, ← sinh_mul_I, mul_assoc, ← sinh_mul_I,
    ← cosh_mul_I, ← cosh_mul_I, sinh_add]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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