English
If there exists a root of Φ_n in Z/pZ with p prime, then the order of the corresponding unit modulo p divides n.
Русский
Если существует корень Φ_n в Z/pZ, возведённый в единицу, то порядок этого элемента по модулю p делит n.
LaTeX
$$$$\operatorname{orderOf}(\,Z/pZ\text{-unit of coprime}) \mid n.$$$$
Lean4
/-- If `(a : ℕ)` is a root of `cyclotomic n (ZMod p)`, then the multiplicative order of `a` modulo
`p` divides `n`. -/
theorem orderOf_root_cyclotomic_dvd {n : ℕ} (hpos : 0 < n) {p : ℕ} [Fact p.Prime] {a : ℕ}
(hroot : IsRoot (cyclotomic n (ZMod p)) (Nat.castRingHom (ZMod p) a)) :
orderOf (ZMod.unitOfCoprime a (coprime_of_root_cyclotomic hpos hroot)) ∣ n :=
by
apply orderOf_dvd_of_pow_eq_one
suffices hpow : eval (Nat.castRingHom (ZMod p) a) (X ^ n - 1 : (ZMod p)[X]) = 0
by
simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow
apply Units.val_eq_one.1
simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]
rw [IsRoot.def] at hroot
rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons,
eval_mul, hroot, zero_mul]
