lean_workbook_plus_23892

Proved

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

For $n=2$ and $z=\frac {-1 + \textrm{i}} {2}$ we have $|z| = \sqrt{2}/2 < 1$ and $z^2+z = -1/2 \in \mathbb{R}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23892  (n z : ℂ)
  (h₀ : n = 2)
  (h₁ : z = (-1 + Complex.I) / 2) :
  z^2 + z = (-1 / 2)   :=  by sorry

Source