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.EisensteinCriterionAux.map_eq_C_mul_X_pow_of_forall_coeff_mem
{R : Type u_1}
[CommRing 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.leadingCoeff) * Polynomial.X ^ f.natDegree
theorem
Polynomial.EisensteinCriterionAux.le_natDegree_of_map_eq_mul_X_pow
{R : Type u_1}
[CommRing R]
{n : ℕ}
{P : Ideal R}
(hP : P.IsPrime)
{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.natDegree
theorem
Polynomial.EisensteinCriterionAux.eval_zero_mem_ideal_of_eq_mul_X_pow
{R : Type u_1}
[CommRing 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 : n ≠ 0)
:
Polynomial.eval 0 q ∈ P
theorem
Polynomial.EisensteinCriterionAux.isUnit_of_natDegree_eq_zero_of_isPrimitive
{R : Type u_1}
[CommRing R]
{p : Polynomial R}
{q : Polynomial R}
(hu : (p * q).IsPrimitive)
(hpm : p.natDegree = 0)
:
IsUnit p
theorem
Polynomial.irreducible_of_eisenstein_criterion
{R : Type u_1}
[CommRing R]
[IsDomain R]
{f : Polynomial R}
{P : Ideal R}
(hP : P.IsPrime)
(hfl : f.leadingCoeff ∉ P)
(hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P)
(hfd0 : 0 < f.degree)
(h0 : f.coeff 0 ∉ P ^ 2)
(hu : f.IsPrimitive)
:
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.