Prove2Me

lean_workbook_plus_82398

Proved

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

proofwiki

Given the roots a,b,ca, b, c of P(x)=x3−2x2+3x−4P(x) = x^3 - 2x^2 + 3x - 4, derive the equation S3−2S2+3S1−4S0=0S_3 - 2S_2 + 3S_1 - 4S_0 = 0 by summing P(a)=0P(a) = 0, P(b)=0P(b) = 0, and P(c)=0P(c) = 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82398 (a b c : ℂ) (ha : a^3 - 2*a^2 + 3*a - 4 = 0) (hb : b^3 - 2*b^2 + 3*b - 4 = 0) (hc : c^3 - 2*c^2 + 3*c - 4 = 0) : a^3 + b^3 + c^3 - 2 * (a^2 + b^2 + c^2) + 3 * (a + b + c) - 4 * 3 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph