Lean-Workbook Plus 25957: Trigonometric identity

Proved

WorkbookRestored.plus_25957

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

lean-workbookrestored-importssource-checked

$\sin(\pi/11)\ne0$ .

Source: Lean-Workbook row lean_workbook_plus_25957 (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_25957 : Real.sin (π / 11) ≠ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_25957; immutable original Prove2Me node bc553a6d-a50c-4894-85fa-3c040767bec2

View graph