# 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 : ), n < f.degreef.coeff n P) :
= Polynomial.C ( f.leadingCoeff) * Polynomial.X ^ f.natDegree
theorem Polynomial.EisensteinCriterionAux.le_natDegree_of_map_eq_mul_X_pow {R : Type u_1} [] {n : } {P : } (hP : P.IsPrime) {q : } {c : Polynomial (R P)} (hq : = c * Polynomial.X ^ n) (hc0 : c.degree = 0) :
n q.natDegree
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 : n 0) :
P
theorem Polynomial.EisensteinCriterionAux.isUnit_of_natDegree_eq_zero_of_isPrimitive {R : Type u_1} [] {p : } {q : } (hu : (p * q).IsPrimitive) (hpm : p.natDegree = 0) :
theorem Polynomial.irreducible_of_eisenstein_criterion {R : Type u_1} [] [] {f : } {P : } (hP : P.IsPrime) (hfl : f.leadingCoeffP) (hfP : ∀ (n : ), n < f.degreef.coeff n P) (hfd0 : 0 < f.degree) (h0 : f.coeff 0P ^ 2) (hu : f.IsPrimitive) :

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.