Commit 2025-04-11 13:00 0ac690b5

feat(RingTheory/Polynomial/Eisenstein/Generalized): a generalized version of the Eisenstein criterion (#23710) A generalized form of the Eisenstein criterion Let R be an integral domain, P a prime ideal of R and let K be the field of fractions o f R ⧸ P. Let q : R[X] be a monic polynomial which is irreducible in K[X]. Let f : R[X] be a monic polynomial of strictly positive degree whose image in K[X] is a power of q. Assume moreover that f.modByMonic q is not zero in (R ⧸ (P ^ 2))[X]. Then f is irreducible. The Eisenstein criterion is the particular case where q := X. The case of a polynomial q := X - a is interesting, then the mod P ^ 2 hypothesis can rephrased as saying that f.derivative.eval a ∉ P ^ 2. (TODO) The case of cyclotomic polynomials of prime index can be proved directly using that, with a = 1. We give a (possibly non convincing) application to the irreducibility of the polynomial X ^ 4 - 10 * X + 1 in ℤ[X]. One argues modulo 3, with q := X ^ 2 + 1.

Remark

The result can also be generalized to the case where the leading coefficients of f and q do not belong to P. (By localization at P, make these coefficients invertible.) There are two obstructions, though :

• Usually, one will only obtain irreducibility in F[X], where F is the field of fractions of R. (If R is a UFD, this will be close to what is wanted, but not in general.)
• The mod P ^ 2 hypothesis will have to be rephrased to a condition in the second symbolic power of P. When P is a maximal ideal, that symbolic power coincides with P ^ 2, but not in general.