lean_workbook_plus_37185

Open

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

We have $\sin^{2}{x} + \sin^{2}{2x} + \sin^{2}{3x} \ + \cos^{2}{x} + \cos^{2}{2x} + \cos^{2}{3x} \ =3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37185 : ∀ x : ℝ, (Real.sin x)^2 + (Real.sin (2 * x))^2 + (Real.sin (3 * x))^2 + (Real.cos x)^2 + (Real.cos (2 * x))^2 + (Real.cos (3 * x))^2 = 3   :=  by sorry

Source

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

View graph