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.eval_zero_mem_ideal_of_eq_mul_X_pow {R : Type u_1} [CommRing R] {n : } {P : Ideal R} {q : Polynomial R} {c : Polynomial (R P)} (hq : Polynomial.map (Ideal.Quotient.mk P) q = c * Polynomial.X ^ n) (hn0 : 0 < n) :
theorem Polynomial.irreducible_of_eisenstein_criterion {R : Type u_1} [CommRing R] [IsDomain R] {f : Polynomial R} {P : Ideal R} (hP : Ideal.IsPrime P) (hfl : ¬Polynomial.leadingCoeff f P) (hfP : ∀ (n : ), n < Polynomial.degree fPolynomial.coeff f n P) (hfd0 : 0 < Polynomial.degree f) (h0 : ¬Polynomial.coeff f 0 P ^ 2) (hu : Polynomial.IsPrimitive f) :

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.