Factorization of cyclotomic polynomials over finite fields

We compute the degree of the irreducible factors of the n-th cyclotomic polynomial over a finite field of characteristic p, where p and n are coprime.

Main results

• Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible : Let K be a finite field of cardinality p ^ f and let P be an irreducible factor of the n-th cyclotomic polynomial over K, where p and n are coprime. Then the degree of P is the multiplicative order of p ^ f modulo n.

theorem Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible {K : Type u_1} [Field K] [Fintype K] {p f n : ℕ} {P : Polynomial K} (hK : Fintype.card K = p ^ f) (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] (hP : P ∣ cyclotomic n K) (hPirr : Irreducible P) : P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)

Let K be a finite field of cardinality p ^ f and let P be an irreducible factor of the n-th cyclotomic polynomial over K, where p and n are coprime. Then the degree of P is the multiplicative order of p ^ f modulo n.

theorem Polynomial.irreducible_of_dvd_cyclotomic_of_natDegree {K : Type u_1} [Field K] [Fintype K] {p f n : ℕ} {P : Polynomial K} (hK : Fintype.card K = p ^ f) (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] (hP : P ∣ cyclotomic n K) (hPdeg : 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.

theorem ZMod.irreducible_of_dvd_cyclotomic_of_natDegree {p n : ℕ} [hp : Fact (Nat.Prime p)] {P : Polynomial (ZMod p)} (hpn : ¬p ∣ n) (hP : P ∣ Polynomial.cyclotomic n (ZMod p)) (hPdeg : P.natDegree = orderOf (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.

theorem Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic {K : Type u_1} [Field K] [Fintype K] {p f n : ℕ} {P : Polynomial K} (hK : Fintype.card K = p ^ f) (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] [DecidableEq K] (hP : P ∈ UniqueFactorizationMonoid.normalizedFactors (cyclotomic n K)) : P.natDegree = orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)

theorem Polynomial.normalizedFactors_cyclotomic_card {K : Type u_1} [Field K] [Fintype K] {p f n : ℕ} (hK : Fintype.card K = p ^ f) (hn : p.Coprime n) [hp : Fact (Nat.Prime p)] [DecidableEq K] : (UniqueFactorizationMonoid.normalizedFactors (cyclotomic n K)).toFinset.card = n.totient / orderOf (ZMod.unitOfCoprime (p ^ f) ⋯)

Let K be a finite field of cardinality p ^ f and let P be an irreducible factor of the n-th cyclotomic polynomial over K, where p and n are coprime. This result computes the number of distinct irreducible factors of cyclotomic n K.