Commit 2024-05-30 06:24 40db2ffc
View on Github →feat(RingTheory/RootsOfUnity/Complex): complex roots of unity have norm 1 (#13352) This adds
lemma Complex.norm_rootOfUnity_eq_one {ζ : ℂˣ} {n : ℕ+} (hζ : ζ ∈ rootsOfUnity n ℂ) :
‖(ζ : ℂ)‖ = 1
feat(RingTheory/RootsOfUnity/Complex): complex roots of unity have norm 1 (#13352) This adds
lemma Complex.norm_rootOfUnity_eq_one {ζ : ℂˣ} {n : ℕ+} (hζ : ζ ∈ rootsOfUnity n ℂ) :
‖(ζ : ℂ)‖ = 1