isPrimitiveRoot_iff' — Mathlib

English

Let k be a positive integer and suppose ζ is a primitive k-th root of unity in a domain R. Then for any ξ in Rˣ (a unit) we have: ξ is a primitive k-th root of unity if and only if there exists an integer i with 0 ≤ i < k, gcd(i,k) = 1, and ξ = ζ^i.

Русский

Пусть k > 0 и ζ — примитивный корень порядка k в ряде R. Тогда для любого ξ, удовлетворяющего ξ^{k} = 1 и не являющегося тривиальным равенством, существует i с 0 ≤ i < k, gcd(i,k) = 1 и ξ = ζ^i, если и только если ξ является примитивным k-ым корнем.

LaTeX

$$$\\operatorname{IsPrimitiveRoot}(\zeta,k) \\Rightarrow\\Big( \\operatorname{IsPrimitiveRoot}(\\xi,k) \\ \\Longleftrightarrow\\ \\exists i

Lean4

theorem isPrimitiveRoot_iff' {k : ℕ} [NeZero k] {ζ ξ : Rˣ} (h : IsPrimitiveRoot ζ k) :
    IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ :=
  by
  constructor
  · intro hξ
    obtain ⟨i, hik, rfl⟩ := h.eq_pow_of_mem_rootsOfUnity hξ.pow_eq_one
    rw [h.pow_iff_coprime <| NeZero.pos k] at hξ
    exact ⟨i, hik, hξ, rfl⟩
  · rintro ⟨i, -, hi, rfl⟩; exact h.pow_of_coprime i hi

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