Prove2Me

lean_workbook_plus_29780

Proved

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

Prove that: ∀z∈C,Re(z)<−12⇒∣1+z2∣>∣1+z+z2∣\forall \mathop {}\limits^{} z \in C\mathop {}\limits^{} ,\mathop {}\limits^{} {\mathop{\rm Re}\nolimits} (z) < - \frac{1}{2}\mathop {}\limits^{} \Rightarrow \mathop {}\limits^{} \left| {1 + {z^2}} \right| > \left| {1 + z + {z^2}} \right|

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29780 (z : ℂ) (h : z.re < -1 / 2) : ‖(1 + z^2)‖ > ‖(1 + z + z^2)‖   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph