lean_workbook_plus_65697

Open

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

And we also have: $\sin{\frac{8\pi}{17}}=\cos{\left(\frac{\pi}{2}-\frac{8\pi}{17} \right)}=\cos{\frac{\pi}{34}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65697 : Real.sin (8 * Real.pi / 17) = Real.cos (Real.pi / 34)   :=  by sorry

Source