lean_workbook_plus_46600

Open

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

Second equation: \n $\rightarrow \cos(x-y)-\cos(x+y)=n \rightarrow 2\cos^{2}\frac{x-y}{2}-2\cos^{2}\frac{x+y}{2}=n$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46600 (x y n : ℝ) : (cos (x - y) - cos (x + y) = n ↔ 2 * cos ((x - y) / 2) ^ 2 - 2 * cos ((x + y) / 2) ^ 2 = n)   :=  by sorry

Source

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

View graph