lean_workbook_plus_8407

Proved

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

Prove that $a^2+b^2\ge ab$ by expressing $a^2+b^2-ab$ as a sum of squares or a fraction of such a sum.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8407 (a b : ℝ) : a ^ 2 + b ^ 2 ≥ a * b   :=  by sorry

Source