lean_workbook_plus_82004

Proved

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

Given $z,w \in C: z + w = 8 + 6i$ and $|z - w| = 4$ , find $|z|^2 + |w|^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82004 (z w : ℂ) (h₁ : z + w = 8 + 6 * Complex.I) (h₂ : ‖z - w‖ = 4) : ‖z‖^2 + ‖w‖^2 = 58   :=  by sorry

Source