Irreducible polynomials over finite fields

For every positive degree, a finite field has a monic irreducible polynomial of that degree. We obtain one as the minimal polynomial of a primitive element of a finite extension of that degree.

Such a polynomial f of degree d over k presents the degree-d extension of k as the quotient k[X] ⧸ (f). Over a prime field ZMod p these polynomials are the irreducible factors from which one assembles polynomials with a prescribed factorization pattern modulo p, as used when reading off cycle types of Galois groups by reduction modulo primes.

Main results

• TauCeti.exists_monic_irreducible_natDegree_eq: a monic irreducible polynomial of any prescribed positive degree over a finite field.
• TauCeti.exists_monic_irreducible_natDegree_eq_ne_X: such a polynomial can be chosen distinct from X.

References

The construction follows Mathlib's finite-field extensions FiniteField.Extension and FiniteField.finrank_extension (Mathlib/FieldTheory/Finite/Extension.lean) and its primitive element theorem Field.exists_primitive_element_of_finite_top (Mathlib/FieldTheory/PrimitiveElement.lean).

theorem TauCeti.exists_monic_irreducible_natDegree_eq (k : Type u_1) [Field k] [Finite k] (d : ℕ) (hd : 0 < d) : ∃ (f : Polynomial k), f.Monic ∧ Irreducible f ∧ f.natDegree = d

For every positive d, there is a monic irreducible polynomial of degree d over any finite field.

theorem TauCeti.exists_monic_irreducible_natDegree_eq_ne_X (k : Type u_1) [Field k] [Finite k] (d : ℕ) (hd : 0 < d) : ∃ (h : Polynomial k), h.Monic ∧ Irreducible h ∧ h.natDegree = d ∧ h ≠ Polynomial.X

For every positive d, a finite field has a monic irreducible polynomial of degree d other than X: in degree 1 take X + 1, and in higher degree any irreducible polynomial differs from X by its degree.