# mathlibdocumentation

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 #

• polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map: A primitive polynomial is irreducible iff it is irreducible in a fraction field.
• polynomial.is_primitive.int.irreducible_iff_irreducible_map_cast: A primitive polynomial over ℤ is irreducible iff it is irreducible over ℚ.
• polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map: Two primitive polynomials divide each other iff they do in a fraction field.
• polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast: Two primitive polynomials over ℤ divide each other if they do in ℚ.
theorem polynomial.is_primitive.is_unit_iff_is_unit_map_of_injective {R : Type u_1} [comm_ring R] [is_domain R] {S : Type u_2} [comm_ring S] [is_domain S] {φ : R →+* S} (hinj : function.injective φ) {f : polynomial R} (hf : f.is_primitive) :
theorem polynomial.is_primitive.irreducible_of_irreducible_map_of_injective {R : Type u_1} [comm_ring R] [is_domain R] {S : Type u_2} [comm_ring S] [is_domain S] {φ : R →+* S} (hinj : function.injective φ) {f : polynomial R} (hf : f.is_primitive) (h_irr : irreducible f)) :
theorem polynomial.is_primitive.is_unit_iff_is_unit_map {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {p : polynomial R} (hp : p.is_primitive) :
theorem polynomial.is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {p : polynomial K} (h0 : p 0)  :
theorem polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map {R : Type u_1} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {p : polynomial R} (hp : p.is_primitive) :

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} [comm_ring R] [is_domain R] {K : Type u_2} [field K] [ K] [ K] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) (h_dvd : p q) :
p q
theorem polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map {R : Type u_1} [comm_ring R] [is_domain R] (K : Type u_2) [field K] [ K] [ K] {p q : polynomial R} (hp : p.is_primitive) (hq : q.is_primitive) :
p q p q

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