lean_workbook_plus_57421

Proved

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

Prove the equality $a\alpha+b\beta+c\gamma = (a+b+c)(\alpha+\beta+\gamma)$ where $\alpha = bc-a^2$ , $\beta = ca-b^2$ , $\gamma = ab-c^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57421 (a b c α β γ : ℝ) (h₁ : α = b * c - a ^ 2) (h₂ : β = c * a - b ^ 2) (h₃ : γ = a * b - c ^ 2) : a * α + b * β + c * γ = (a + b + c) * (α + β + γ)   :=  by sorry

Source

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

View graph