eq_pow_of_mem_rootsOfUnity — Mathlib

English

If ζ is primitive and ξ is a root of unity, then there exists i < k with ζ^i = ξ.

Русский

Если ζ примитивен и ξ — корень единицы, существует i < k такое, что ζ^i = ξ.

LaTeX

$$IsPrimitiveRoot(ζ, k) → ξ ∈ rootsOfUnity(k, R) → ∃ i < k, ζ^i = ξ$$

Lean4

theorem eq_pow_of_mem_rootsOfUnity {k : ℕ} [NeZero k] {ζ ξ : Rˣ} (h : IsPrimitiveRoot ζ k) (hξ : ξ ∈ rootsOfUnity k R) :
    ∃ i < k, ζ ^ i = ξ :=
  by
  obtain ⟨n, rfl⟩ : ∃ n : ℤ, ζ ^ n = ξ := by rwa [← h.zpowers_eq] at hξ
  have hk0 : (0 : ℤ) < k := mod_cast NeZero.pos k
  let i := n % k
  have hi0 : 0 ≤ i := Int.emod_nonneg _ (ne_of_gt hk0)
  lift i to ℕ using hi0 with i₀ hi₀
  refine ⟨i₀, ?_, ?_⟩
  · zify; rw [hi₀]; exact Int.emod_lt_of_pos _ hk0
  · rw [← zpow_natCast, hi₀, ← Int.emod_add_mul_ediv n k, zpow_add, zpow_mul, h.zpow_eq_one, one_zpow, mul_one]

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