English
If h is a primitive root ζ of order k and i is coprime to k, then ζ^i is a primitive root of order k.
Русский
Пусть h — примитивный корень ζ порядка k, и i взаимно простым с k; тогда ζ^i — примитивный корень того же порядка k.
LaTeX
$$$$\text{If } h: \ IsPrimitiveRoot(\zeta, k) \text{ and } \gcd(i,k)=1, \text{ then } IsPrimitiveRoot(\zeta^i, k).$$$$
Lean4
theorem pow_of_coprime (h : IsPrimitiveRoot ζ k) (i : ℕ) (hi : i.Coprime k) : IsPrimitiveRoot (ζ ^ i) k :=
by
by_cases h0 : k = 0
· subst k; simp_all only [pow_one, Nat.coprime_zero_right]
rcases h.isUnit h0 with ⟨ζ, rfl⟩
rw [← Units.val_pow_eq_pow_val]
rw [coe_units_iff] at h ⊢
refine
{ pow_eq_one := by rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]
dvd_of_pow_eq_one := fun l hl ↦ h.dvd_of_pow_eq_one l ?_ }
rw [← pow_one ζ, ← zpow_natCast ζ, ← hi.gcd_eq_one, Nat.gcd_eq_gcd_ab, zpow_add, mul_pow, ← zpow_natCast, ← zpow_mul,
mul_right_comm]
simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_natCast]
