Prove2Me

lean_workbook_plus_75088

Proved

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

Solve z2+(2i−3)z+(5−i)=0 z^2+(2i-3)z+(5-i)=0 write the solutions in Cartesian and polar form.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75088 (z : ℂ) : (z^2 + (2 * Complex.I - 3) * z + (5 - Complex.I) = 0) ↔ (z = 1 + Complex.I ∨ z = 2 - 3 * Complex.I)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph