mathlib3 documentation

ring_theory.polynomial.selmer

Irreducibility of Selmer Polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

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

source
theorem polynomial.X_pow_sub_X_sub_one_irreducible_aux {n : ℕ} (z : ℂ) :
¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)
source
theorem polynomial.X_pow_sub_X_sub_one_irreducible {n : ℕ} (hn1 : n ≠ 1) :
irreducible (polynomial.X ^ n - polynomial.X - 1)
source
theorem polynomial.X_pow_sub_X_sub_one_irreducible_rat {n : ℕ} (hn1 : n ≠ 1) :
irreducible (polynomial.X ^ n - polynomial.X - 1)