# mathlib3documentation

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 #

• is_integrally_closed.eq_map_mul_C_of_dvd: if R is integrally closed, 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
• polynomial.monic.irreducible_iff_irreducible_map_fraction_map: A monic polynomial over an integrally closed domain is irreducible iff it is irreducible in a fraction field
• is_integrally_closed_iff': Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomials
• polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map: A primitive polynomial over a GCD domain 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 over a GCD domain 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 integral_closure.mem_lifts_of_monic_of_dvd_map {R : Type u_1} [comm_ring R] (K : Type u_2) [field K] [ K] {f : polynomial R} (hf : f.monic) {g : polynomial K} (hg : g.monic) (hd : g f) :
theorem is_integrally_closed.eq_map_mul_C_of_dvd {R : Type u_1} [comm_ring R] (K : Type u_2) [field K] [ K] [is_domain R] [ K] {f : polynomial R} (hf : f.monic) {g : polynomial K} (hg : g f) :
(g' : , g' * = g

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

theorem polynomial.is_primitive.is_unit_iff_is_unit_map {R : Type u_1} [comm_ring R] {K : Type u_2} [field K] [ K] [ K] {p : polynomial R} (hp : p.is_primitive) :

Gauss's Lemma for integrally closed domains states that a monic polynomial is irreducible iff it is irreducible in the fraction field.

theorem polynomial.is_integrally_closed_iff' {R : Type u_1} [comm_ring R] {K : Type u_2} [field K] [ K] [ K] [is_domain R] :

Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomials

theorem polynomial.monic.dvd_of_fraction_map_dvd_fraction_map {R : Type u_1} [comm_ring R] {K : Type u_2} [field K] [ K] [ K] [is_domain R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) (h : q p) :
q p
theorem polynomial.monic.dvd_iff_fraction_map_dvd_fraction_map {R : Type u_1} [comm_ring R] {K : Type u_2} [field K] [ K] [ K] [is_domain R] {p q : polynomial R} (hp : p.monic) (hq : q.monic) :
q p q p
theorem polynomial.is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part {R : Type u_1} [comm_ring R] {K : Type u_2} [field K] [ K] [ K] [is_domain R] {p : polynomial K} (h0 : p 0)  :

Gauss's Lemma for GCD domains 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] {K : Type u_2} [field K] [ K] [ K] [is_domain R] {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] (K : Type u_2) [field K] [ K] [ K] [is_domain R] {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 ℚ.