lean_workbook_plus_28301

Open

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

Lemma. For any $\theta$ , $\cos\left(\theta\right)+\cos\left(\theta+\frac{2\pi}{3}\right)+\cos\left(\theta+\frac{4\pi}{3}\right)=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28301 (θ : ℝ) : Real.cos θ + Real.cos (θ + (2 * Real.pi / 3)) + Real.cos (θ + (4 * Real.pi / 3)) = 0   :=  by sorry

Source