Prove2Me

lean_workbook_plus_33549

Proved

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

Find the solutions of the equation: z2−8(1−i)z+63−16i=0z^2-8(1-i)z+63-16i=0

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

View graph