two_mul_cos_mul_cos

Mathlib.Analysis.Complex.Trigonometric

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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