Lean-Workbook Plus 57418: Trigonometric inequality

Proved

WorkbookRestored.plus_57418

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

lean-workbookrestored-importssource-checked

For a natural number $n$ with $0<n<9$ , $\cos(n\pi/9)+\cos((9-n)\pi/9)=0$ .

Source: Lean-Workbook row lean_workbook_plus_57418 (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_57418 (n : ℕ) (hn : 0 < n ∧ n < 9) : Real.cos (n * π / 9) + Real.cos ((9 - n) * π / 9) = 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_57418; immutable original Prove2Me node b6851f55-3b3d-4258-b320-cb80cfc12628

View graph