Eisenstein's criterion #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.degree → f.coeff n ∈ P) :
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}
[comm_ring R]
{n : ℕ}
{P : ideal R}
(hP : P.is_prime)
{q : polynomial R}
{c : polynomial (R ⧸ P)}
(hq : polynomial.map (ideal.quotient.mk P) q = c * polynomial.X ^ n)
(hc0 : 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}
[comm_ring 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) :
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}
[comm_ring R]
{p q : polynomial R}
(hu : ∀ (x : R), ⇑polynomial.C x ∣ p * q → is_unit x)
(hpm : p.nat_degree = 0) :
is_unit p
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.degree → f.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.