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}
[integral_domain R]
{f : polynomial R}
{P : ideal R} :
(∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P) → f ≠ 0 → polynomial.map (ideal.quotient.mk P) f = ⇑polynomial.C (⇑(ideal.quotient.mk P) f.leading_coeff) * polynomial.X ^ f.nat_degree
theorem
polynomial.eisenstein_criterion_aux.le_nat_degree_of_map_eq_mul_X_pow
{R : Type u_1}
[integral_domain R]
{n : ℕ}
{P : ideal R}
(hP : P.is_prime)
{q : polynomial R}
{c : polynomial P.quotient} :
polynomial.map (ideal.quotient.mk P) q = c * polynomial.X ^ n → c.degree = 0 → n ≤ q.nat_degree
theorem
polynomial.eisenstein_criterion_aux.eval_zero_mem_ideal_of_eq_mul_X_pow
{R : Type u_1}
[integral_domain R]
{n : ℕ}
{P : ideal R}
{q : polynomial R}
{c : polynomial P.quotient} :
polynomial.map (ideal.quotient.mk P) q = c * polynomial.X ^ n → 0 < n → polynomial.eval 0 q ∈ P
theorem
polynomial.eisenstein_criterion_aux.is_unit_of_nat_degree_eq_zero_of_forall_dvd_is_unit
{R : Type u_1}
[integral_domain R]
{p q : polynomial R} :
(∀ (x : R), ⇑polynomial.C x ∣ p * q → is_unit x) → p.nat_degree = 0 → is_unit p
theorem
polynomial.irreducible_of_eisenstein_criterion
{R : Type u_1}
[integral_domain R]
{f : polynomial R}
{P : ideal R} :
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.