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]
[normalized_gcd_monoid R]
{S : Type u_2}
[comm_ring S]
[is_domain S]
{φ : R →+* S}
(hinj : function.injective ⇑φ)
{f : R[X]}
(hf : f.is_primitive) :
is_unit f ↔ is_unit (polynomial.map φ f)
theorem
polynomial.is_primitive.irreducible_of_irreducible_map_of_injective
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{S : Type u_2}
[comm_ring S]
[is_domain S]
{φ : R →+* S}
(hinj : function.injective ⇑φ)
{f : R[X]}
(hf : f.is_primitive)
(h_irr : irreducible (polynomial.map φ f)) :
theorem
polynomial.is_primitive.is_unit_iff_is_unit_map
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
{p : R[X]}
(hp : p.is_primitive) :
is_unit p ↔ is_unit (polynomial.map (algebra_map R K) p)
theorem
polynomial.is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
{p : K[X]}
(h0 : p ≠ 0)
(h : is_unit (is_localization.integer_normalization R⁰ p).prim_part) :
is_unit p
theorem
polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
{p : R[X]}
(hp : p.is_primitive) :
irreducible p ↔ irreducible (polynomial.map (algebra_map R K) p)
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]
[normalized_gcd_monoid R]
{K : Type u_2}
[field K]
[algebra R K]
[is_fraction_ring R K]
{p q : R[X]}
(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
theorem
polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map
{R : Type u_1}
[comm_ring R]
[is_domain R]
[normalized_gcd_monoid R]
(K : Type u_2)
[field K]
[algebra R K]
[is_fraction_ring R K]
{p q : R[X]}
(hp : p.is_primitive)
(hq : q.is_primitive) :
p ∣ q ↔ polynomial.map (algebra_map R K) p ∣ polynomial.map (algebra_map R K) q
theorem
polynomial.is_primitive.int.irreducible_iff_irreducible_map_cast
{p : ℤ[X]}
(hp : p.is_primitive) :
Gauss's Lemma for ℤ states that a primitive integer polynomial is irreducible iff it is
irreducible over ℚ.
theorem
polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast
(p q : ℤ[X])
(hp : p.is_primitive)
(hq : q.is_primitive) :
p ∣ q ↔ polynomial.map (int.cast_ring_hom ℚ) p ∣ polynomial.map (int.cast_ring_hom ℚ) q