two_mul_sin_mul_sin

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Real.two_mul_sin_mul_sin

English

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

Русский

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

LaTeX

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

Lean4

theorem two_mul_sin_mul_sin (x y : ℝ) : 2 * sin x * sin y = cos (x - y) - cos (x + y) :=
  by
  simp [cos_add, cos_sub]
  ring

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

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

Разделы

Аффилиация

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