lean_workbook_plus_61326
ProvedSo we need when
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61326 (a : ℝ) (ha : 0 ≤ a) : 3 * a ^ 4 - 6 * a ^ 3 + 8 * a ^ 2 - 6 * a + 3 ≥ 0 := by sorry
Source
So we need when
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61326 (a : ℝ) (ha : 0 ≤ a) : 3 * a ^ 4 - 6 * a ^ 3 + 8 * a ^ 2 - 6 * a + 3 ≥ 0 := by sorry