lean_workbook_plus_57418

Open

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

Derive the identity: $\cos\frac {n\pi}{9} + \cos\frac {(9 - n)\pi}{9} = 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57418 (n : ℕ) (hn : 0 < n ∧ n < 9) : Real.cos (n * π / 9) + Real.cos ((9 - n) * π / 9) = 0   :=  by sorry

Source