lean_workbook_plus_75631
ProvedProve for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75631 (a : ℝ) (h : a ≥ 1) : 4 * a ^ 3 - 9 * a ^ 2 + 9 * a + 4 ≥ 0 := by sorry
Source
Prove for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_75631 (a : ℝ) (h : a ≥ 1) : 4 * a ^ 3 - 9 * a ^ 2 + 9 * a + 4 ≥ 0 := by sorry