Theorems · Theorem · commutative algebra

Polynomial.generalizedEisenstein

∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {K : Type u_2} [inst_2 : Field K] [inst_3 : Algebra R K]
  {q f : Polynomial R} {p : ℕ},
  Irreducible (Polynomial.map (algebraMap R K) q) →
    q.Monic →
      f.IsPrimitive →
        0 < f.natDegree →
          (algebraMap R K) f.leadingCoeff ≠ 0 →
            Polynomial.map (algebraMap R K) f =
                Polynomial.C ((algebraMap R K) f.leadingCoeff) * Polynomial.map (algebraMap R K) q ^ p →
              Polynomial.map (Ideal.Quotient.mk (RingHom.ker (algebraMap R K) ^ 2)) (f %ₘ q) ≠ 0 → Irreducible f

A generalized Eisenstein criterion Let R be an integral domain and K an R-algebra which is a domain. Let q : R[X] be a monic polynomial which is prime in K[X]. Let f : R[X] be a primitive polynomial of strictly positive degree whose leading coefficient is not zero in K and such that the image f in K[X] is a power of q. Assume moreover that f.modByMonic q is not zero in (R ⧸ (P ^ 2))[X], where P is the kernel of algebraMap R K. Then f is irreducible.

Defined in

Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFieldAlgebra