Polynomials over an irreducible ring

This file contains results about the polynomials over an irreducible ring (i.e. a ring with only one minimal prime ideal, equivalently, whose spectrum is an irreducible topological space).

Main results

• Polynomial.Monic.irreducible_of_irreducible_map_of_isPrime_nilradical: a monic polynomial over an irreducible ring is irreducible if it is irreducible after mapping into an integral domain. A generalization to Polynomial.Monic.irreducible_of_irreducible_map.

Tags

polynomial, irreducible ring, nilradical, prime ideal

theorem Polynomial.Monic.irreducible_of_irreducible_map_of_isPrime_nilradical {R : Type u_1} {S : Type u_2} [CommRing R] [Ideal.IsPrime (nilradical R)] [CommRing S] [IsDomain S] (φ : R →+* S) (f : Polynomial R) (hm : Polynomial.Monic f) (hi : Irreducible (Polynomial.map φ f)) : Irreducible f

A polynomial over an irreducible ring R is irreducible if it is monic and irreducible after mapping into an integral domain S (https://math.stackexchange.com/a/4843432/235999). A generalization to Polynomial.Monic.irreducible_of_irreducible_map.