English
Let h be a primitive root ζ of order k with k>0. For any i, IsPrimitiveRoot(ζ^i, k) holds if and only if gcd(i,k)=1.
Русский
Пусть h — примитивный корень ζ порядка k, где k>0. Для любого i выполняется IsPrimitiveRoot(ζ^i, k) тогда и только тогда, когда gcd(i,k)=1.
LaTeX
$$$$k>0 \Rightarrow (IsPrimitiveRoot(\zeta^i, k) \iff \gcd(i,k)=1).$$$$
Lean4
theorem pow_iff_coprime (h : IsPrimitiveRoot ζ k) (h0 : 0 < k) (i : ℕ) : IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k :=
by
refine ⟨fun hi ↦ ?_, h.pow_of_coprime i⟩
obtain ⟨a, ha⟩ := i.gcd_dvd_left k
obtain ⟨b, hb⟩ := i.gcd_dvd_right k
suffices b = k by rwa [this, eq_comm, Nat.mul_eq_right h0.ne', ← Nat.coprime_iff_gcd_eq_one] at hb
rw [ha] at hi
rw [mul_comm] at hb
apply Nat.dvd_antisymm ⟨i.gcd k, hb⟩ (hi.dvd_of_pow_eq_one b _)
rw [← pow_mul', ← mul_assoc, ← hb, pow_mul, h.pow_eq_one, one_pow]
