Mapping irreducible polynomials #
Main results #
Monic.irreducible_of_irreducible_map: we can prove a monic polynomial is irreducible by mapping it to another integral domain and checking for irreducibility there.
theorem
Polynomial.Monic.irreducible_of_irreducible_map
{R : Type u}
{S : Type v}
[CommRing R]
[IsDomain R]
[CommRing S]
[IsDomain S]
(φ : R →+* S)
(f : Polynomial R)
(h_mon : f.Monic)
(h_irr : Irreducible (Polynomial.map φ f))
:
A polynomial over an integral domain R is irreducible if it is monic and
irreducible after mapping into an integral domain S.
A special case of this lemma is that a polynomial over ℤ is irreducible if
it is monic and irreducible over ℤ/pℤ for some prime p.