lean_workbook_plus_50110

Proved

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

Using the identity, $m^3+n^3+3mn(m+n)=(m+n)^3$ , $m^3+n^3+3mn=1$ becomes $(m+n)^3-3mn(m+n)+3mn=1$ . Factoring yields: $(m+n-1)(m^2+n^2-mn+m+n+1)=0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50110  (m n : ℂ)
  (h₀ : m^3 + n^3 + 3 * m * n = 1) :
  (m + n - 1) * (m^2 + n^2 - m * n + m + n + 1) = 0   :=  by sorry

Source