lean_workbook_plus_8064

Proved

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

Let $x+y+z=s$ , $xy+yz+xz=q$ . It is $s^2 \ge 3q$ . The original is equivalent to $(s^2-3q)(s^2-q) \ge 0$ , which is obvious. Equality iff $x=y=z$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8064 (x y z s q : ℝ) (hx : x + y + z = s) (hy : x*y + y*z + z*x = q) : s^2 ≥ 3*q   :=  by sorry

Source