lean_workbook_plus_3567

Proved

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

Let $a,b,c$ be real numbers with sum equal to zero. Prove that $ab^3+bc^3+ca^3\leqslant 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3567 (a b c : ℝ) (hab : a + b + c = 0) : a * b ^ 3 + b * c ^ 3 + c * a ^ 3 ≤ 0   :=  by sorry

Source