lean_workbook_plus_45433

Proved

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

If $a,b$ are distinct roots of $x^{4}+x+1=0$ , prove that $a^4+a+1=b^4+b+1=0$ and $a^3+a^2b+ab^2+b^3=-1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45433 {a b : ℂ} (hab : a ≠ b) (h : a^4 + a + 1 = 0) (h' : b^4 + b + 1 = 0) : a^3 + a^2*b + a*b^2 + b^3 = -1   :=  by sorry

Source