# Documentation

Mathlib.RingTheory.Polynomial.GaussLemma

# Gauss's Lemma #

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

## Main Results #

• IsIntegrallyClosed.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.leadingCoeff⁻¹) 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
• isIntegrallyClosed_iff': Integrally closed domains are precisely the domains for in which Gauss's lemma holds for monic polynomials
• Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map: A primitive polynomial over a GCD domain is irreducible iff it is irreducible in a fraction field
• Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast: A primitive polynomial over ℤ is irreducible iff it is irreducible over ℚ.
• Polynomial.IsPrimitive.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.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast: Two primitive polynomials over ℤ divide each other if they do in ℚ.
theorem integralClosure.mem_lifts_of_monic_of_dvd_map {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] {f : } (hf : ) {g : } (hg : ) (hd : g Polynomial.map () f) :
theorem IsIntegrallyClosed.eq_map_mul_C_of_dvd {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] {f : } (hf : ) {g : } (hg : g Polynomial.map () f) :
g', Polynomial.map () g' * Polynomial.C () = g

If K = Frac(R) and g : K[X] divides a monic polynomial with coefficients in R, then g * (C g.leadingCoeff⁻¹) has coefficients in R

theorem Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective {R : Type u_1} [] {S : Type u_2} [] [] {φ : R →+* S} (hinj : ) {f : } (hf : ) :
theorem Polynomial.IsPrimitive.irreducible_of_irreducible_map_of_injective {R : Type u_1} [] {S : Type u_2} [] [] {φ : R →+* S} (hinj : ) {f : } (hf : ) (h_irr : ) :
theorem Polynomial.IsPrimitive.isUnit_iff_isUnit_map {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] {p : } (hp : ) :
theorem Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] {p : } (h : ) :

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

theorem Polynomial.isIntegrallyClosed_iff' {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] [] :
∀ (p : ), → ( Irreducible (Polynomial.map () p))

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} [] {K : Type u_2} [] [Algebra R K] [] {p : } {q : } (hp : ) (hq : ) (h : Polynomial.map () q Polynomial.map () p) :
q p
theorem Polynomial.Monic.dvd_iff_fraction_map_dvd_fraction_map {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] {p : } {q : } (hp : ) (hq : ) :
theorem Polynomial.isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] [] {p : } (h0 : p 0) :
theorem Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] [] {p : } (hp : ) :

Gauss's Lemma for GCD domains states that a primitive polynomial is irreducible iff it is irreducible in the fraction field.

theorem Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map {R : Type u_1} [] {K : Type u_2} [] [Algebra R K] [] [] {p : } {q : } (hp : ) (hq : ) (h_dvd : Polynomial.map () p Polynomial.map () q) :
p q
theorem Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map {R : Type u_1} [] (K : Type u_2) [] [Algebra R K] [] [] {p : } {q : } (hp : ) (hq : ) :

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

theorem Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (p : ) (q : ) (hp : ) (hq : ) :
p q