The eighth cyclotomic polynomial modulo primes

The Galois group of X⁴ + 1 has label 4T2: it is the Klein four-group, acting on the four roots by even permutations. An irreducible reduction modulo a prime would give a four-cycle in this action, which is odd. Thus X⁴ + 1 is reducible modulo every prime, even though it is irreducible over ℚ.

theorem TauCeti.quarticFactSplitsSplittingField (f : Polynomial ℚ) : Fact (Polynomial.map (algebraMap ℚ f.SplittingField) f).Splits

@[simp]

theorem TauCeti.not_irreducible_X_pow_four_add_one (p : ℕ) [Fact (Nat.Prime p)] : ¬Irreducible (Polynomial.X ^ 4 + 1)

The eighth cyclotomic polynomial X⁴ + 1 becomes reducible modulo every prime. Its Galois action over ℚ has label 4T2, so every induced permutation is even, whereas an irreducible reduction would exhibit an odd four-cycle.