lean_workbook_plus_16072

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove the identity $\cos 2kx \cdot \cos x = \frac {1}{2}\left[\cos \left(2k - 1\right)x + \cos \left(2k + 1\right)x\right]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16072 : ∀ k x, Real.cos (2 * k * x) * Real.cos x = (1 / 2) * (Real.cos ((2 * k - 1) * x) + Real.cos ((2 * k + 1) * x))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph