Polynomial.irreducible_of_eisenstein_criterion

theorem Polynomial.irreducible_of_eisenstein_criterion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {f : Polynomial R} {P : Ideal R}, P.IsPrime → f.leadingCoeff ∉ P → (∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P) → 0 < f.degree → f.coeff 0 ∉ P ^ 2 → f.IsPrimitive → Irreducible f

The theorem, known as the Eisenstein Criterion, states that given a commutative ring `R` that is also a domain, a non-constant polynomial `f` with coefficients in `R`, and a prime ideal `P` in `R`, if all coefficients of `f` except the leading coefficient are in `P`, and the trailing coefficient is not in the square of `P`, and no non-units in `R` divide `f`, then `f` is irreducible. This criterion is a crucial test for determining the irreducibility of polynomials.

More concisely: If `R` is a commutative domain, `f(X)` is a non-constant polynomial in `R[X]` with leading coefficient a unit, and the coefficients of `f(X)` except the leading one belong to some prime ideal `P` of `R`, while the constant term does not belong to `P^2`, then `f(X)` is irreducible in `R[X]`.