English
Let K be a finite field with q = p^f elements and let P be a factor of cyclotomic n over K with gcd(p, n) = 1. If the degree of P equals the multiplicative order of p^f modulo n, then P is irreducible.
Русский
Пусть K — конечное поле с q = p^f элементами и P — фактор cyclotomic n над K при gcd(p, n) = 1. Если deg P равен мультипликативному порядку p^f по модулю n, то P неприводим.
LaTeX
$$$$ \\text{If } P \\mid \\operatorname{cyclotomic}(n, K), \\; \\gcd(p, n) = 1, \\ \\deg P = \\operatorname{orderOf}(p^f) \\Rightarrow P \\text{ irreducible}. $$$$
Lean4
/-- Let `K` be a finite field of cardinality `p ^ f` and let `P` be a factor of the `n`-th
cyclotomic polynomial over `K`, where `p` and `n` are coprime. If the degree of `P` is
the multiplicative order of `p ^ f` modulo `n` then `P` is irreducible. -/
theorem irreducible_of_dvd_cyclotomic_of_natDegree (hP : P ∣ cyclotomic n K)
(hPdeg : P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f))) : Irreducible P := by
classical
have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
obtain ⟨Q, HQ⟩ :=
exists_mem_normalizedFactors hP0 <|
not_isUnit_of_natDegree_pos _ <|
pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
refine
(associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
(irreducible_of_normalized_factor Q HQ)
rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_ (irreducible_of_normalized_factor Q HQ)]
exact
dvd_of_mem_normalizedFactors <|
mem_of_le ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ
