mathlib documentation

ring_theory.eisenstein_criterion

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.irreducible_of_eisenstein_criterion {R : Type u_1} [integral_domain R] {f : polynomial R} {P : ideal R} :
P.is_primef.leading_coeff P(∀ (n : ), n < f.degreef.coeff n P)0 < f.degreef.coeff 0 P ^ 2(∀ (x : R), polynomial.C x fis_unit x)irreducible 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.