lean_workbook_plus_18566

Proved

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

Given that $a, b, c, d$ are reals such that $a+b+c+d=0 \ ab+bc+cd+da=0 \ ab+ac+ad+bc+bd+cd=0 \ a^3+b^3+c^3+d^3=0$ prove that $a=b=c=d=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18566 (a b c d : ℝ) (h1 : a+b+c+d=0) (h2 : a*b+b*c+c*d+d*a=0) (h3 : a*b + a*c + a*d + b*c + b*d + c*d=0) (h4 : a^3+b^3+c^3+d^3=0) : a=0 ∧ b=0 ∧ c=0 ∧ d=0   :=  by sorry

Source

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

View graph