English
Let p be prime and p ∤ n. If a polynomial P over Z/pZ divides cyclotomic n, and deg P equals the order of the unit modulo n, then P is irreducible.
Русский
Пусть p — простое число и p не делит n. Если P делит cyclotomic n (Z/pZ) и deg P равен порядку единицы по модулю n, то P неразложим.
LaTeX
$$$$ P \\mid \\operatorname{cyclotomic}(n, \\mathbb{Z}/p\\mathbb{Z}) \\quad \\text{and} \\quad \\deg P = \\operatorname{orderOf}(\\text{unitOfCoprime}(_ , p)) \\Rightarrow P \\text{ irreducible}. $$$$
Lean4
/-- Let `P` be a factor of the `n`-th cyclotomic polynomial over `ZMod p`, where `p` does not divide
`n`. If the degree of `P` is the multiplicative order of `p` modulo `n` then `P` is
irreducible. -/
theorem _root_.ZMod.irreducible_of_dvd_cyclotomic_of_natDegree {P : (ZMod p)[X]} (hpn : ¬p ∣ n)
(hP : P ∣ cyclotomic n (ZMod p))
(hPdeg : P.natDegree = orderOf (unitOfCoprime _ (hp.1.coprime_iff_not_dvd.mpr hpn))) : Irreducible P :=
Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree (f := 1) (p := p) (by simp)
(by simpa using hp.1.coprime_iff_not_dvd.mpr hpn) hP (by simpa)
