lean_workbook_plus_16613

Proved

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

Let $a>0$ be a real number and let $z\ne 0$ be a complex number so that $\left|z+\frac 1z\right|=a$ . Find the range of $|z|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16613 (a : ℝ) (ha : 0 < a) (z : ℂ) (hz : z ≠ 0) (h : ‖z + 1/z‖ = a) : ‖z‖ ∈ Set.Ioi 0 ∪ Set.Ioi a   :=  by sorry

Source