lean_workbook_plus_77615

Open

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

Claim. If $u+v+w=0$ , then $\cos(u)^2+\cos(v)^2+\cos(w)^2=1+2\cos(u) \cos(v) \cos(w)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77615 (u v w : ℂ) (h : u + v + w = 0) :
  Complex.cos u ^ 2 + Complex.cos v ^ 2 + Complex.cos w ^ 2 =
    1 + 2 * Complex.cos u * Complex.cos v * Complex.cos w   :=  by sorry

Source

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

View graph