norm_eq_one_of_pow_eq_one — Mathlib

English

If ζ^n = 1 for some complex ζ and natural n with n ≠ 0, then the ordinary norm of ζ is 1; i.e., |ζ| = 1.

Русский

Если ζ^n = 1 для некоторого ζ ∈ ℂ и натурального n, причём n ≠ 0, то |ζ| = 1.

LaTeX

$$$ (\\zeta^{n} = 1) \\land (n \\neq 0) \\Rightarrow |\\zeta| = 1 $$$

Lean4

theorem norm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) : ‖ζ‖ = 1 :=
  congr_arg Subtype.val (nnnorm_eq_one_of_pow_eq_one h hn)

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