arg_eq_zero_iff — Mathlib

English

Let h be a primitive root with n ≠ 0. Then ζ.arg = 0 if and only if ζ = 1.

Русский

Пусть ζ — примитивный корень с n ≠ 0. Тогда ζ.arg = 0 тогда и только тогда, когда ζ = 1.

LaTeX

$$IsPrimitiveRoot_arg_eq_zero_iff: IsPrimitiveRoot ζ n → Ne n 0 → (ζ.arg = 0) ↔ (ζ = 1)$$

Lean4

theorem arg_eq_zero_iff {n : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ n) (hn : n ≠ 0) : ζ.arg = 0 ↔ ζ = 1 :=
  ⟨fun h => hζ.arg_ext IsPrimitiveRoot.one hn one_ne_zero (h.trans Complex.arg_one.symm), fun h =>
    h.symm ▸ Complex.arg_one⟩

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