lean_workbook_plus_16796
ProvedFor , prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16796 (a : ℝ) (ha : 0 < a) : (1 + a^2 + a^4)^4 ≥ 9 * a^4 * (a + a^2 + a^3)^2 := by sorry
Source
For , prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_16796 (a : ℝ) (ha : 0 < a) : (1 + a^2 + a^4)^4 ≥ 9 * a^4 * (a + a^2 + a^3)^2 := by sorry