lean_workbook_plus_9318

Open

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

Prove that $\cos (\frac{\pi}{2}) + \cos (\frac{3 \pi}{2}) = 0+ 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9318 : Real.cos (π / 2) + Real.cos (3 * π / 2) = 0 + 0   :=  by sorry

Source