lean_workbook_plus_33234

Open

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

For the next equation letting $x + \frac{\pi}{4} = \alpha$ we have $\sin{\alpha} = 0$ . This occurs when $\alpha = k\pi$ with $k$ being an integer. So $x = \alpha - \frac{\pi}{4} = k\pi - \frac{\pi}{4}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33234  (x : ℝ)
  (h₀ : Real.sin (x + Real.pi / 4) = 0) :
  ∃ k : ℤ, x = k * Real.pi - Real.pi / 4   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph