Polynomial.IsEisensteinAt.irreducible

theorem Polynomial.IsEisensteinAt.irreducible : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {𝓟 : Ideal R} {f : Polynomial R}, f.IsEisensteinAt 𝓟 → 𝓟.IsPrime → f.IsPrimitive → 0 < f.natDegree → Irreducible f

The theorem states that for any commutative ring `R` which is also an integral domain, any ideal `𝓟` in `R`, and any polynomial `f` with coefficients in `R`, if `f` satisfies the Eisenstein criterion at `𝓟`, `𝓟` is a prime ideal, and `f` is primitive (i.e., the greatest common divisor of its coefficients is 1), then `f` is irreducible if its degree is positive. The Eisenstein criterion is a condition on the coefficients of the polynomial, used to prove its irreducibility.

More concisely: If `R` is a commutative ring and an integral domain, `I` is an ideal in `R`, `f` is a primitive polynomial over `R` of positive degree satisfying the Eisenstein criterion at `I`, then `I` is a prime ideal and `f` is irreducible.