Theorems · Theorem · commutative algebra

Polynomial.irreducible_of_eisenstein_criterion

∀ {R : Type u_1} [inst : CommRing R] [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

If f is a nonconstant 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 nonunits in R divide f, then f is irreducible.

Defined in

Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Cited by

1 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain