lean_workbook_plus_30158

Proved

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

Prove that there are no non-zero complex numbers z satisfying $|z+1|\leq 1$ , $|z^2+1|\leq 1$ and $|z^3+1|\leq 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_30158 (z : ℂ) (hz1 : z ≠ 0) (hz2 : ‖z + 1‖ ≤ 1) (hz3 : ‖z^2 + 1‖ ≤ 1) (hz4 : ‖z^3 + 1‖ ≤ 1) : False   :=  by sorry

Source