lean_workbook_plus_81117

Proved

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

Given $a + b + c = u$ , $ab + bc + ca = v$ , $abc = w$ , then $a^4 + b^4 + c^4 = u^4 - 4u^2v + 2v^2 + 4uw$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81117 (a b c u v w : ℂ) (h1 : a + b + c = u) (h2 : a * b + b * c + c * a = v) (h3 : a * b * c = w) : a ^ 4 + b ^ 4 + c ^ 4 = u ^ 4 - 4 * u ^ 2 * v + 2 * v ^ 2 + 4 * u * w   :=  by sorry

Source

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

View graph