lean_workbook_plus_24293

Proved

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

Let $\alpha, \beta, \gamma, \delta$ be the roots of the equation $x^4+px^3+qx^2+rx+s=0$ . Prove that $(\alpha\beta+\gamma\delta)(\beta\gamma+\alpha\delta)(\gamma\alpha+\beta\delta)=r^2-4qs+p^2s$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24293 (α β γ δ : ℂ) (p q r s : ℂ) (h : α + β + γ + δ = -p) (h' : α * β + α * γ + α * δ + β * γ + β * δ + γ * δ = q) (h'' : α * β * γ + α * β * δ + α * γ * δ + β * γ * δ = -r) (h''' : α * β * γ * δ = s) : (α * β + γ * δ) * (β * γ + α * δ) * (γ * α + β * δ) = r^2 - 4*q*s + p^2 * s   :=  by sorry

Source

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

View graph