Irreducibility survives the affine primitive-part reduction

theorem NairTenenbaum.affineRestriction_irreducible_map {Q : Polynomial ℤ} (hQ : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {M : ℤ} (hM : M ≠ 0) (a : ℤ) : Irreducible (Polynomial.map (Int.castRingHom ℚ) (affineRestriction Q M a))

theorem NairTenenbaum.affineRestriction_primPart_irreducible_map {Q : Polynomial ℤ} (hQ : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {M : ℤ} (hM : M ≠ 0) (a : ℤ) : Irreducible (Polynomial.map (Int.castRingHom ℚ) (affineRestriction Q M a).primPart)

theorem NairTenenbaum.exists_affine_primitive_reduction {Q : Polynomial ℤ} (hQ : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) : ∃ (M : ℕ), 0 < M ∧ ∀ (a : ℤ), NoFixedPrimeDivisor (affineRestriction Q (↑M) a).primPart ∧ Irreducible (Polynomial.map (Int.castRingHom ℚ) (affineRestriction Q (↑M) a).primPart)