Theorems · Theorem · number theory

ZMod.irreducible_of_dvd_cyclotomic_of_natDegree

∀ {p n : ℕ} [hp : Fact (Nat.Prime p)] {P : Polynomial (ZMod p)} (hpn : ¬p ∣ n),
  P ∣ Polynomial.cyclotomic n (ZMod p) → P.natDegree = orderOf (ZMod.unitOfCoprime p ⋯) → Irreducible P

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.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Cited by

0 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact