mathlib documentation

ring_theory.polynomial.gauss_lemma

Gauss's Lemma #

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

Main Results #

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 .