Theorems · Theorem · number theory

Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree

∀ {K : Type u_1} [inst : Field K] [inst_1 : Fintype K] {p f n : ℕ} {P : Polynomial K},
  Fintype.card K = p ^ f →
    ∀ (hn : p.Coprime n) [hp : Fact (Nat.Prime p)],
      P ∣ Polynomial.cyclotomic n K → P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯) → Irreducible P

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.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFintypeFact