English
For k>0, h primitive root of order k, i is natural, IsPrimitiveRoot(ζ^i,k) iff gcd(i,k)=1.
Русский
Для k>0, если ζ — примитивный корень порядка k, то IsPrimitiveRoot(ζ^i,k) эквивалентно gcd(i,k)=1.
LaTeX
$$$$k>0 \Rightarrow ( IsPrimitiveRoot(\zeta^i,k) \iff \gcd(i,k)=1 ).$$$$
Lean4
/-- If there is an `n`-th primitive root of unity in `R` and `b` divides `n`,
then there is a `b`-th primitive root of unity in `R`. -/
theorem pow {n : ℕ} {a b : ℕ} (hn : 0 < n) (h : IsPrimitiveRoot ζ n) (hprod : n = a * b) : IsPrimitiveRoot (ζ ^ a) b :=
by
subst n
simp only [iff_def, ← pow_mul, h.pow_eq_one, true_and]
intro l hl
exact Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_mul_pos_right hn) <| h.dvd_of_pow_eq_one _ hl
