lean_workbook_plus_7806

Proved

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

Given $\sum_{cyc}a = 0$ and $\sum_{cyc}ab = \frac{3}{2}$ , prove that $\sum_{cyc}a^2 = \frac{-3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7806 (a b c : ℝ) (h : a + b + c = 0) (h' : a * b + b * c + c * a = 3 / 2) : a ^ 2 + b ^ 2 + c ^ 2 = -3   :=  by sorry

Source