# 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} [comm_ring R] {f : polynomial R} {P : ideal R} (hfP : ∀ (n : ), n < f.degreef.coeff n P) :
theorem polynomial.eisenstein_criterion_aux.le_nat_degree_of_map_eq_mul_X_pow {R : Type u_1} [comm_ring R] {n : } {P : ideal R} (hP : P.is_prime) {q : polynomial R} {c : polynomial (R P)} (hq : = c * ) (hc0 : c.degree = 0) :
theorem polynomial.eisenstein_criterion_aux.eval_zero_mem_ideal_of_eq_mul_X_pow {R : Type u_1} [comm_ring R] {n : } {P : ideal R} {q : polynomial R} {c : polynomial (R P)} (hq : = c * ) (hn0 : 0 < n) :
P
theorem polynomial.eisenstein_criterion_aux.is_unit_of_nat_degree_eq_zero_of_forall_dvd_is_unit {R : Type u_1} [comm_ring R] {p q : polynomial R} (hu : ∀ (x : R), p * q) (hpm : p.nat_degree = 0) :
theorem polynomial.irreducible_of_eisenstein_criterion {R : Type u_1} [comm_ring R] [is_domain R] {f : polynomial R} {P : ideal R} (hP : P.is_prime) (hfl : f.leading_coeff P) (hfP : ∀ (n : ), n < f.degreef.coeff n P) (hfd0 : 0 < f.degree) (h0 : f.coeff 0 P ^ 2) (hu : f.is_primitive) :

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.