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.

theorem polynomial.X_pow_sub_X_sub_one_irreducible_aux {n : } (z : ) :
¬(z ^ n = z + 1 z ^ n + z ^ 2 = 0)