nnnorm_eq_one_of_pow_eq_one — Mathlib

English

If ζ^n = 1 for some complex ζ and natural n with n ≠ 0, then the nonnegative norm of ζ equals 1; i.e., ‖ζ‖₊ = 1.

Русский

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

LaTeX

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

Lean4

theorem nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) : ‖ζ‖₊ = 1 :=
  (pow_left_inj₀ zero_le' zero_le' hn).1 <| by rw [← nnnorm_pow, h, nnnorm_one, one_pow]

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