Documentation

Mathlib.RingTheory.Polynomial.GaussLemma

Gauss's Lemma #

Gauss's Lemma is one of a few results pertaining to irreducibility of primitive polynomials.

Main Results #

theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] {f : Polynomial R} (hf : Polynomial.Monic f) {g : Polynomial K} (hg : g Polynomial.map (algebraMap R K) f) :
g', Polynomial.map (algebraMap R K) g' * Polynomial.C (Polynomial.leadingCoeff g) = g

If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leadingCoeff⁻¹) has coefficients in R

Gauss's Lemma for integrally closed domains states that a monic polynomial is irreducible iff it is irreducible in the fraction field.

Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomials

Gauss's Lemma for GCD domains states that a primitive polynomial is irreducible iff it is irreducible in the fraction field.

Gauss's Lemma for states that a primitive integer polynomial is irreducible iff it is irreducible over .