The norm of an integer power of a complex number
ProvedWorkbookSource.problem_33186lean-workbooksource-checked
For every complex number z and integer n, ‖zⁿ‖=‖z‖ⁿ.
Source: InternLM Lean-Workbook, record lean_workbook_33186 (Apache-2.0). The complete source proposition and variable types are retained.
Preamble
import Mathlib open Complex
Formal statement
theorem WorkbookSource.problem_33186 (z : ℂ) (n : ℤ) : ‖z^n‖ = ‖z‖^n := by sorry
Source