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 : polynomial R}
(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 : polynomial R}
(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 : polynomial R}
(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 : polynomial K}
(h0 : p ≠ 0)
(h : is_unit (is_localization.integer_normalization (non_zero_divisors 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 : polynomial R}
(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 : 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
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 : polynomial R}
(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 : polynomial ℤ}
(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 : polynomial ℤ)
(hp : p.is_primitive)
(hq : q.is_primitive) :
p ∣ q ↔ polynomial.map (int.cast_ring_hom ℚ) p ∣ polynomial.map (int.cast_ring_hom ℚ) q