lean_workbook_plus_44215

Proved

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

$a^2+b^2 \ge 2ab, \ b^2+c^2 \ge 2bc, \ c^2+a^2 \ge 2ca$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44215 (a b c: ℝ) : a^2 + b^2 ≥ 2*a*b ∧ b^2 + c^2 ≥ 2*b*c ∧ c^2 + a^2 ≥ 2*c*a   :=  by sorry

Source