Irreducibility of Selmer Polynomials

This file proves irreducibility of the Selmer polynomials X ^ n - X - 1.

Main results

• X_pow_sub_X_sub_one_irreducible: The Selmer polynomials X ^ n - X - 1 are irreducible.

TODO: Show that the Selmer polynomials have full Galois group.

theorem Polynomial.X_pow_sub_X_sub_one_irreducible_aux {n : ℕ} (z : ℂ) : ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)

theorem Polynomial.X_pow_sub_X_sub_one_irreducible {n : ℕ} (hn1 : n ≠ 1) : Irreducible (Polynomial.X ^ n - Polynomial.X - 1)

theorem Polynomial.X_pow_sub_X_sub_one_irreducible_rat {n : ℕ} (hn1 : n ≠ 1) : Irreducible (Polynomial.X ^ n - Polynomial.X - 1)