lean_workbook_plus_65364
ProvedProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65364 (a : ℝ) : (a - 1) ^ 2 * (85 * a ^ 4 - 294 * a ^ 3 + 506 * a ^ 2 - 438 * a + 213) ≥ 0 := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_65364 (a : ℝ) : (a - 1) ^ 2 * (85 * a ^ 4 - 294 * a ^ 3 + 506 * a ^ 2 - 438 * a + 213) ≥ 0 := by sorry