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 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 .