mathlib3 documentation

ring_theory.polynomial.gauss_lemma

Gauss's Lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main Results #

theorem integral_closure.mem_lifts_of_monic_of_dvd_map {R : Type u_1} [comm_ring R] (K : Type u_2) [field K] [algebra R K] {f : polynomial R} (hf : f.monic) {g : polynomial K} (hg : g.monic) (hd : g polynomial.map (algebra_map R K) f) :

If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leading_coeff⁻¹) 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 .