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.

theorem polynomial.is_primitive.dvd_of_fraction_map_dvd_fraction_map {R : Type u_1} [integral_domain R] [gcd_monoid R] {K : Type u_2} [field K] [algebra R K] [is_fraction_ring R K] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) (h_dvd : polynomial.map (algebra_map R K) p polynomial.map (algebra_map R K) q) :
p q

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