Lean-Workbook Plus 77615: Trigonometric identity

Proved

WorkbookRestored.plus_77615

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For complex $u,v,w$ with $u+v+w=0$ , $\cos^2u+\cos^2v+\cos^2w=1+2\cos u\cos v\cos w$ .

Source: Lean-Workbook row lean_workbook_plus_77615 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real

Formal statement

theorem WorkbookRestored.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/blob/main/lean_workbook.json, row lean_workbook_plus_77615; immutable original Prove2Me node 8541e09a-2a34-4c26-bd19-b5ae139294bf

View graph