lean_workbook_plus_43044
Provedprove that for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_43044 (x : ℝ) (hx : x ≥ 3) : (x - 3) * (x^3 + 3 * x^2 + 9 * x - 27) ≥ 0 := by sorry
Source
prove that for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_43044 (x : ℝ) (hx : x ≥ 3) : (x - 3) * (x^3 + 3 * x^2 + 9 * x - 27) ≥ 0 := by sorry