Theorem Complex.norm_eq_one_of_mem_rootOfUnity

Modification history

2024-05-31 13:35
Mathlib/RingTheory/RootsOfUnity/Complex.lean
feat: add API for additive characters (#13389) …
Deleted Complex.norm_eq_one_of_mem_rootOfUnityView on Github →
2024-05-30 06:24
Mathlib/RingTheory/RootsOfUnity/Complex.lean
feat(RingTheory/RootsOfUnity/Complex): complex roots of unity have norm 1 (#13352) …
Added Complex.norm_eq_one_of_mem_rootOfUnityView on Github →