norm_eq_one_of_mem_rootsOfUnity — Mathlib

English

If ζ is a unit root of unity, its complex norm equals 1.

Русский

Если ζ является корнем единицы в виде единицы (обратимый), тогда его комплексная норма равна 1.

LaTeX

$$norm_eq_one_of_mem_rootsOfUnity: hζ ∈ rootsOfUnity n ℂ → ‖(ζ : ℂ)‖ = 1$$

Lean4

theorem norm_eq_one_of_mem_rootsOfUnity {ζ : ℂˣ} {n : ℕ} [NeZero n] (hζ : ζ ∈ rootsOfUnity n ℂ) : ‖(ζ : ℂ)‖ = 1 :=
  by
  refine norm_eq_one_of_pow_eq_one ?_ <| NeZero.ne n
  norm_cast
  rw [_root_.mem_rootsOfUnity] at hζ
  rw [hζ, Units.val_one]

Похожие утверждения