lean_workbook_plus_79877

Proved

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

Let's first get rid of the indices and write $a+b+c=p+q+r=ap+bq+cr=0$ . If we consider $b,c,q,r$ as fixed then $a,p$ are defined by $a=-(b+c),p=-(q+r)$ and the ensuing condition is $ap+bq+cr=0\iff 2bq+br+cq+2cr=0$ . Assuming $cr\not=0$ we divide by $cr$ and find $2(b/c)(q/r)+(b/c)+(q/r)+2=0$ . With $\alpha:=b/c,\beta:=q/r$ we have $(2\alpha+1)(2\beta+1)=-3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79877  (a b c p q r : ℝ)
  (h₀ : a + b + c = 0)
  (h₁ : p + q + r = 0)
  (h₂ : a * p + b * q + c * r = 0)
  (h₃ : c ≠ 0) :
  (2 * b * q + b * r + c * q + 2 * c * r = 0)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph