Prove2Me

lean_workbook_plus_10616

Proved

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

We have c=−a−bc = -a-b and a2+b2+c2=1⇔ab+bc+ca=−12⇔ab=−12+c2{a^2} + {b^2} + {c^2} = 1 \Leftrightarrow ab + bc + ca = - \frac{1}{2} \Leftrightarrow ab = - \frac{1}{2} + {c^2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10616  (a b c : ℝ)
  (h₀ : c = -(a + b))
  (h₁ : a^2 + b^2 + c^2 = 1) :
  a * b = -1 / 2 + c^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph