lean_workbook_plus_70840

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that for all real numbers $x,y$ excluding 0: $x^4 + x^{3}y + x^{2}y^{2} + x y^{3} + y^4 > 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70840 {x y : ℝ} (hx : x ≠ 0) (hy : y ≠ 0) : x^4 + x^3*y + x^2*y^2 + x*y^3 + y^4 > 0   :=  by sorry

Source