zpow_of_gcd_eq_one — Mathlib

English

If h is a primitive root ζ of order k and i ∈ Z with gcd(i,k)=1, then ζ^i is a primitive k-th root.

Русский

Пусть h — примитивный корень ζ порядка k; если i ∈ Z и gcd(i,k)=1, то ζ^i — примитивный корень порядка k.

LaTeX

$$IsPrimitiveRoot(\\zeta, k) \\land gcd(i, k) = 1 \\Rightarrow IsPrimitiveRoot(\\zeta^i, k)$$

Lean4

theorem zpow_of_gcd_eq_one (h : IsPrimitiveRoot ζ k) (i : ℤ) (hi : i.gcd k = 1) : IsPrimitiveRoot (ζ ^ i) k :=
  by
  by_cases h0 : 0 ≤ i
  · lift i to ℕ using h0
    exact_mod_cast h.pow_of_coprime i hi
  have : 0 ≤ -i := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
  lift -i to ℕ using this with i' hi'
  rw [← inv_iff, ← zpow_neg, ← hi', zpow_natCast]
  apply h.pow_of_coprime
  rwa [Int.gcd, ← Int.natAbs_neg, ← hi'] at hi

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