Residue roots of primitive integral polynomials

theorem NairTenenbaum.primitive_map_zmod_ne_zero {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) : Polynomial.map (Int.castRingHom (ZMod p)) Q ≠ 0

theorem NairTenenbaum.rootCount_le_reduction_degree {Q : Polynomial ℤ} {p : ℕ} (hp : Nat.Prime p) (hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ≠ 0) : rootCount Q p ≤ (Polynomial.map (Int.castRingHom (ZMod p)) Q).natDegree

theorem NairTenenbaum.primitive_rootCount_le_degree {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) : rootCount Q p ≤ Q.natDegree

theorem NairTenenbaum.primitive_rootCount_lt_of_degree_lt {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) (hdeg : Q.natDegree < p) : rootCount Q p < p

theorem NairTenenbaum.primitive_noFixedPrimeDivisor_of_degree_le_one {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (hdeg : Q.natDegree ≤ 1) : NoFixedPrimeDivisor Q