lean_workbook_plus_32073

Open

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

Prove that $cos^4x=\frac{1}{8}cos4x+\frac{1}{2}cos2x+\frac{3}{8}$ using the trigonometric form of a complex number.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32073 (x : ℝ) : (cos x)^4 = 1 / 8 * cos (4 * x) + 1 / 2 * cos (2 * x) + 3 / 8   :=  by sorry

Source