lean_workbook_plus_50860

Open

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

either $\cos x=\frac{\pi}2+\sin x+2k\pi$ $\iff$ $\cos(x+\frac{\pi}4)=\frac{(4k+1)\pi}{2\sqrt 2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50860 (x : ℝ) (k : ℤ) : (Real.cos x = Real.pi / 2 + Real.sin x + 2 * Real.pi * k) ↔ (Real.cos (x + Real.pi / 4) = (2 * Real.sqrt 2)⁻¹ * (4 * k + 1) * Real.pi)   :=  by sorry

Source

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

View graph