arg_ext — Mathlib

English

If two primitive roots have the same argument and nonzero orders, then they are equal.

Русский

Если два примитивных корня имеют одинаковый аргумент и ненулевые порядки, то они равны.

LaTeX

$$∀ {n m : Nat} {ζ μ : Complex}, IsPrimitiveRoot ζ n → IsPrimitiveRoot μ m → Ne n 0 → Ne m 0 → ζ.arg = μ.arg → ζ = μ$$

Lean4

theorem arg_ext {n m : ℕ} {ζ μ : ℂ} (hζ : IsPrimitiveRoot ζ n) (hμ : IsPrimitiveRoot μ m) (hn : n ≠ 0) (hm : m ≠ 0)
    (h : ζ.arg = μ.arg) : ζ = μ :=
  Complex.ext_norm_arg ((hζ.norm'_eq_one hn).trans (hμ.norm'_eq_one hm).symm) h

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