English
If there is a root a of cyclotomic n in Z/pZ with p prime, then a and p are coprime.
Русский
Если существует корень a циклотоми́ческого n в Z/pZ, где p простое, то a и p взаимно простые.
LaTeX
$$$$\gcd(a,p) = 1 \quad\Rightarrow\quad a \text{ is a root of } \mathrm{cyclotomic}_n(\mathbb{Z}/p\mathbb{Z}).$$$$
Lean4
/-- If `(a : ℕ)` is a root of `cyclotomic n (ZMod p)`, where `p` is a prime, then `a` and `p` are
coprime. -/
theorem coprime_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : Fact p.Prime] {a : ℕ}
(hroot : IsRoot (cyclotomic n (ZMod p)) (Nat.castRingHom (ZMod p) a)) : a.Coprime p :=
by
apply Nat.Coprime.symm
rw [hprime.1.coprime_iff_not_dvd]
intro h
replace h := (ZMod.natCast_eq_zero_iff a p).2 h
rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot
by_cases hone : n = 1
·
simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero, one_ne_zero,
coeff_sub] at hroot
rw [cyclotomic_coeff_zero (ZMod p)
(Nat.succ_le_of_lt (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at hroot
exact one_ne_zero hroot
