English
Let K be a finite field with q = p^f elements and gcd(p, n) = 1. If P is a factor of cyclotomic n over K and its natDegree equals the order of p^f modulo n, then P is irreducible.
Русский
Пусть K — конечное поле с q = p^f элементами и gcd(p, n) = 1. Если P делит cyclotomic n над K и natDegree P равен порядку p^f по модулю n, то P неразложим.
LaTeX
$$$$ P \\mid \\operatorname{cyclotomic}(n, K) \\wedge P\\text{ natDegree } P = \\operatorname{orderOf}(p^f) \\Rightarrow P \\text{ irreducible}. $$$$
Lean4
theorem isRoot_of_unity_of_root_cyclotomic {ζ : R} {i : ℕ} (hi : i ∈ n.divisors) (h : (cyclotomic i R).IsRoot ζ) :
ζ ^ n = 1 := by
rcases n.eq_zero_or_pos with (rfl | hn)
· exact pow_zero _
have := congr_arg (eval ζ) (prod_cyclotomic_eq_X_pow_sub_one hn R).symm
rw [eval_sub, eval_X_pow, eval_one] at this
convert eq_add_of_sub_eq' this
convert (add_zero (M := R) _).symm
apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h
exact Finset.dvd_prod_of_mem _ hi
