eq_pow_of_pow_eq_one — Mathlib

English

If ξ^k = 1 and ζ is primitive of order k, then there exists i<k with ζ^i = ξ.

Русский

Если ξ^k = 1 и ζ примитивный порядка k, то существует i<k с ζ^i = ξ.

LaTeX

$$IsPrimitiveRoot(ζ, k) ∧ ξ^k = 1 → ∃ i < k, ζ^i = ξ$$

Lean4

theorem eq_pow_of_pow_eq_one {k : ℕ} [NeZero k] {ζ ξ : R} (h : IsPrimitiveRoot ζ k) (hξ : ξ ^ k = 1) :
    ∃ i < k, ζ ^ i = ξ := by
  lift ζ to Rˣ using h.isUnit NeZero.out
  lift ξ to Rˣ using .of_pow_eq_one hξ <| NeZero.ne k
  simp only [← Units.val_pow_eq_pow_val, ← Units.ext_iff]
  rw [coe_units_iff] at h
  exact h.eq_pow_of_mem_rootsOfUnity <| (mem_rootsOfUnity' k ξ).mpr hξ

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