lean_workbook_plus_2619
ProvedRearrange to
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2619 (x : ℝ) : x^2 * abs (x - 1) ≤ x^4 + x^2 + 1 := by sorry
Source
Rearrange to
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2619 (x : ℝ) : x^2 * abs (x - 1) ≤ x^4 + x^2 + 1 := by sorry