# mathlibdocumentation

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.eisenstein_criterion_aux.map_eq_C_mul_X_pow_of_forall_coeff_mem {R : Type u_1} {f : polynomial R} {P : ideal R} :
(∀ (n : ), n < f.degreef.coeff n P)f 0 =

theorem polynomial.eisenstein_criterion_aux.le_nat_degree_of_map_eq_mul_X_pow {R : Type u_1} {n : } {P : ideal R} (hP : P.is_prime) {q : polynomial R} {c : polynomial P.quotient} :
= c * c.degree = 0n q.nat_degree

theorem polynomial.eisenstein_criterion_aux.eval_zero_mem_ideal_of_eq_mul_X_pow {R : Type u_1} {n : } {P : ideal R} {q : polynomial R} {c : polynomial P.quotient} :
= c * 0 < n P

theorem polynomial.irreducible_of_eisenstein_criterion {R : Type u_1} {f : polynomial R} {P : ideal R} :
P.is_prime(∀ (n : ), n < f.degreef.coeff n P)0 < f.degreef.coeff 0 P ^ 2(∀ (x : R), is_unit x)

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.