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 < Polynomial.degree f → Polynomial.coeff f n ∈ P)
:
Polynomial.map (Ideal.Quotient.mk P) f = ↑Polynomial.C (↑(Ideal.Quotient.mk P) (Polynomial.leadingCoeff f)) * Polynomial.X ^ Polynomial.natDegree f
theorem
Polynomial.EisensteinCriterionAux.le_natDegree_of_map_eq_mul_X_pow
{R : Type u_1}
[CommRing R]
{n : ℕ}
{P : Ideal R}
(hP : Ideal.IsPrime P)
{q : Polynomial R}
{c : Polynomial (R ⧸ P)}
(hq : Polynomial.map (Ideal.Quotient.mk P) q = c * Polynomial.X ^ n)
(hc0 : Polynomial.degree c = 0)
:
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 : 0 < n)
:
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 : Polynomial.IsPrimitive (p * q))
(hpm : Polynomial.natDegree p = 0)
:
IsUnit p
theorem
Polynomial.irreducible_of_eisenstein_criterion
{R : Type u_1}
[CommRing R]
[IsDomain R]
{f : Polynomial R}
{P : Ideal R}
(hP : Ideal.IsPrime P)
(hfl : ¬Polynomial.leadingCoeff f ∈ P)
(hfP : ∀ (n : ℕ), ↑n < Polynomial.degree f → Polynomial.coeff f n ∈ P)
(hfd0 : 0 < Polynomial.degree f)
(h0 : ¬Polynomial.coeff f 0 ∈ P ^ 2)
(hu : Polynomial.IsPrimitive f)
:
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.