# Documentation

Mathlib.RingTheory.EisensteinCriterion

# Eisenstein's criterion #

A proof of a slight generalisation of Eisenstein's criterion for the irreducibility of a polynomial over an integral domain.

theorem Polynomial.EisensteinCriterionAux.map_eq_C_mul_X_pow_of_forall_coeff_mem {R : Type u_1} [] {f : } {P : } (hfP : ∀ (n : ), P) :
= Polynomial.C (↑() ()) * Polynomial.X ^
theorem Polynomial.EisensteinCriterionAux.le_natDegree_of_map_eq_mul_X_pow {R : Type u_1} [] {n : } {P : } (hP : ) {q : } {c : Polynomial (R P)} (hq : = c * Polynomial.X ^ n) (hc0 : ) :
theorem Polynomial.EisensteinCriterionAux.eval_zero_mem_ideal_of_eq_mul_X_pow {R : Type u_1} [] {n : } {P : } {q : } {c : Polynomial (R P)} (hq : = c * Polynomial.X ^ n) (hn0 : 0 < n) :
P
theorem Polynomial.irreducible_of_eisenstein_criterion {R : Type u_1} [] [] {f : } {P : } (hP : ) (hfl : ) (hfP : ∀ (n : ), P) (hfd0 : ) (h0 : ¬ P ^ 2) (hu : ) :

If f is a non constant polynomial with coefficients in R, and P is a prime ideal in R, then if every coefficient in R except the leading coefficient is in P, and the trailing coefficient is not in P^2 and no non units in R divide f, then f is irreducible.