arg_eq_pi_iff — Mathlib

English

If h is a primitive root of order n ≠ 0, then ζ.arg = π iff ζ = −1.

Русский

Если h — примитивный корень порядка n ≠ 0, тогда ζ.arg = π тогда и только тогда, когда ζ = −1.

LaTeX

$$IsPrimitiveRoot_arg_eq_pi_iff: IsPrimitiveRoot ζ n → Ne n 0 → (ζ.arg = π) ↔ (ζ = −1)$$

Lean4

theorem arg_eq_pi_iff {n : ℕ} {ζ : ℂ} (hζ : IsPrimitiveRoot ζ n) (hn : n ≠ 0) : ζ.arg = Real.pi ↔ ζ = -1 :=
  ⟨fun h => hζ.arg_ext (IsPrimitiveRoot.neg_one 0 two_ne_zero.symm) hn two_ne_zero (h.trans Complex.arg_neg_one.symm),
    fun h => h.symm ▸ Complex.arg_neg_one⟩

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