Degrees of factors modulo a prime

This module works out Polynomial.factorDegrees explicitly for X ^ 5 - X - 1, whose reduction splits as a cubic times a quadratic modulo 2 and stays irreducible modulo 5. The generic polynomial carrier and API live in TauCeti/RingTheory/Polynomial/FactorDegrees.lean.

Main declarations

• Polynomial.irreducible_X_sq_add_X_add_one_zmod_two, Polynomial.irreducible_X_pow_three_add_X_sq_add_one_zmod_two: the two irreducibility facts over ZMod 2 that the modulo 2 example rests on.
• Polynomial.irreducible_X_pow_five_sub_X_sub_one_zmod_five: the irreducibility fact over ZMod 5 that the modulo 5 example rests on.
• Polynomial.factorDegrees_X_pow_five_sub_X_sub_one_two: the worked example factorDegrees (X ^ 5 - X - 1) 2 = {3, 2}.
• Polynomial.factorDegrees_X_pow_five_sub_X_sub_one_five: the worked example factorDegrees (X ^ 5 - X - 1) 5 = {5}.

References

• D. A. Marcus, Number Fields, 2nd edition, Springer 2018, Chapter 4, where the factorization of f mod p is matched with the splitting of p.
• J. Neukirch, Algebraic Number Theory, Springer 1999, Chapter I, §8.

The factorization of X ^ 5 - X - 1 modulo 2 and 5

theorem Polynomial.irreducible_X_sq_add_X_add_one_zmod_two : Irreducible (X ^ 2 + X + 1)

X ^ 2 + X + 1 is irreducible over ZMod 2: it is quadratic and has no root there.

theorem Polynomial.irreducible_X_pow_three_add_X_sq_add_one_zmod_two : Irreducible (X ^ 3 + X ^ 2 + 1)

X ^ 3 + X ^ 2 + 1 is irreducible over ZMod 2: it is cubic and has no root there.

theorem Polynomial.factorDegrees_X_pow_five_sub_X_sub_one_two : (X ^ 5 - X - 1).factorDegrees 2 = {3, 2}

The polynomial X ^ 5 - X - 1 has factor degrees 3 and 2 modulo 2: its reduction is the product of the irreducibles X ^ 3 + X ^ 2 + 1 and X ^ 2 + X + 1.

theorem TauCeti.factPrimeFive : Fact (Nat.Prime 5)

theorem Polynomial.irreducible_X_pow_five_sub_X_sub_one_zmod_five : Irreducible (X ^ 5 - X - 1)

X ^ 5 - X - 1 is irreducible over ZMod 5.

theorem Polynomial.factorDegrees_X_pow_five_sub_X_sub_one_five : (X ^ 5 - X - 1).factorDegrees 5 = {5}

The polynomial X ^ 5 - X - 1 is irreducible modulo 5, so its sole factor degree is 5.