lean_workbook_plus_32641

Proved

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

Find $z_1,\ z_2,\ z_3\in\mathbb{C}$ such that $|z_1|=|z_2|=|z_3|=a,\ z_1z_2z_3=a^3,\ a\in\mathbb{R},\ a>0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32641 (a : ℝ) (ha : 0 < a) : ∃ z1 z2 z3 : ℂ, ‖z1‖ = a ∧ ‖z2‖ = a ∧ ‖z3‖ = a ∧ z1 * z2 * z3 = a ^ 3   :=  by sorry

Source