Prove2Me

lean_workbook_plus_72234

Proved

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

Why is f(z)=1z2−1f(z)=\frac{1}{z^2-1} considered to have two isolated singularities - two simple poles at z=1z=1 and z=−1z=-1?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72234 : ∀ z : ℂ, (z^2 - 1)⁻¹ = 0 ↔ z = 1 ∨ z = -1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph