Nonconstant prime polynomials remain prime when coefficients are localized. This also proves preservation of irreducibility under purely transcendental coefficient extension, using a swap of the two polynomial variable families.

theorem CCDN.prime_mvPolynomial_map_localization {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S] (hM : M ≤ nonZeroDivisors R) (f : MvPolynomial σ R) (hf : Prime f) (hd : 0 < f.totalDegree) : Prime ((MvPolynomial.map (algebraMap R S)) f)

Prime polynomials of positive variable degree survive coefficient localization at nonzero elements.

theorem CCDN.irreducible_mvPolynomial_map_fraction_parameters {K : Type u_1} {F : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Field F] [Algebra (MvPolynomial τ K) F] [IsFractionRing (MvPolynomial τ K) F] (f : MvPolynomial σ K) (hf : Irreducible f) (hd : 0 < f.totalDegree) : Irreducible ((MvPolynomial.map ((algebraMap (MvPolynomial τ K) F).comp MvPolynomial.C)) f)

Irreducibility survives adjoining algebraically independent parameters and then passing to their rational function field.