lean_workbook_plus_26539
ProvedThis one is equal to
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_26539 : ∀ a : ℝ, (a - 1) ^ 2 * (a ^ 2 - a + 6) ≥ 0 := by sorry
Source
This one is equal to
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_26539 : ∀ a : ℝ, (a - 1) ^ 2 * (a ^ 2 - a + 6) ≥ 0 := by sorry