lean_workbook_plus_727
OpenGiven , where is an nth root of unity, prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_727 (n : ℕ) (hn : n ≠ 0) : ‖(1 : ℂ) ^ (1 / n : ℂ)‖ = 1 := by sorry
Source
Given , where is an nth root of unity, prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_727 (n : ℕ) (hn : n ≠ 0) : ‖(1 : ℂ) ^ (1 / n : ℂ)‖ = 1 := by sorry