lean_workbook_plus_57988
Open24\cos^4\frac{n\pi}{9}\leq9\cos^2\frac{n\pi}{9}+16\cos^6\frac{n\pi}{9}$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57988 (n : ℤ) : 24 * (cos (n * π / 9))^4 ≤ 9 * (cos (n * π / 9))^2 + 16 * (cos (n * π / 9))^6 := by sorry
Source