Prove2Me

lean_workbook_plus_53231

Proved

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

Let z=(3+4i)(2−2i)(3−i)5iz=\frac{(3+4i)(\sqrt 2-\sqrt 2i)}{(\sqrt 3-i)\sqrt 5i}. Find ∣z∣|z|.\n∣z∣=5|z|=\sqrt{5} ??

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53231 (z : ℂ) (h : z = (3 + 4 * Complex.I) * (Real.sqrt 2 - Real.sqrt 2 * Complex.I) / ((Real.sqrt 3 - Complex.I) * Real.sqrt 5 * Complex.I)) : ‖z‖ = Real.sqrt 5   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph