Prove2Me

lean_workbook_plus_60537

Proved

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

Schur's inequality ∑cyca(a−b)(a−c)⩾0\sum_\text{cyc} a(a-b)(a-c) \geqslant 0 is equivalent to ∑cyc6a(a−b)(a−c)⩾0\sum_\text{cyc} 6a(a-b)(a-c) \geqslant 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60537 {a b c : ℝ} : a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b) ≥ 0 ↔ 6 * a * (a - b) * (a - c) + 6 * b * (b - a) * (b - c) + 6 * c * (c - a) * (c - b) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph