lean_workbook_plus_40378

Proved

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

Find the roots of the equation $(s-t)^n = t$ for $s = 1$ and $n = 5$ , i.e., solve $-t^5 + 5t^4 - 10t^3 + 10t^2 - 6t + 1 = 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40378 (t : ℂ) : (1 - t)^5 = t ↔ -t^5 + 5 * t^4 - 10 * t^3 + 10 * t^2 - 6 * t + 1 = 0   :=  by sorry

Source