lean_workbook_plus_31408

Proved

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

Prove that, if $z$ is a complex number and $n$ is a positive integer, then $\mid z^{n} \mid = \mid z \mid ^{n}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31408 (z : ℂ) (n : ℕ) : ‖z^n‖ = ‖z‖^n   :=  by sorry

Source