lean_workbook_plus_1487
ProvedIt is also
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1487 (a b : ℝ) : (a^2 * b + a * b^2 - 2 * b^3)^2 + (a^3 - 2 * b^3 + a * b^2)^2 ≥ 0 := by sorry
Source
It is also
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1487 (a b : ℝ) : (a^2 * b + a * b^2 - 2 * b^3)^2 + (a^3 - 2 * b^3 + a * b^2)^2 ≥ 0 := by sorry