lean_workbook_plus_76080

Proved

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

$(a - b)^4 + (b - c)^4 + (c - a)^4 \ge 0$ ? Or more generally $(a - b)^{2n} + (b - c)^{2n} + (c - a)^{2n} \ge 0$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76080 (a b c : ℝ) (n : ℕ) : (a - b) ^ (2 * n) + (b - c) ^ (2 * n) + (c - a) ^ (2 * n) ≥ 0   :=  by sorry

Source