Uniform prime-power roots for primitive polynomials

Fixed prime divisors are allowed. The discriminant separates the primes with simple reduction from the finite set requiring a larger bound.

theorem NairTenenbaum.simple_roots_of_discr_primitive {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p : ℕ} (hp : Nat.Prime p) (hD : ↑Q.discr ≠ 0) (a : ResidueRoots Q p) : Polynomial.eval₂ (Int.castRingHom (ZMod p)) (↑a) (Polynomial.derivative Q) ≠ 0

theorem NairTenenbaum.rootCount_prime_pow_le_of_discr_primitive {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) {p ν : ℕ} (hp : Nat.Prime p) (hν : ν ≠ 0) (hD : ↑Q.discr ≠ 0) : rootCount Q (p ^ ν) ≤ rootCount Q p

The uniform prime-power bound away from the discriminant, including primes dividing the leading coefficient.

theorem NairTenenbaum.rootCount_prime_pow_le_discr_cube {Q : Polynomial ℤ} (hD : Q.discr ≠ 0) {p : ℕ} (hp : Nat.Prime p) (hpD : p ∣ Q.discr.natAbs) (ν : ℕ) : rootCount Q (p ^ ν) ≤ Q.discr.natAbs ^ 3

theorem NairTenenbaum.primitive_rootCount_prime_pow_uniform {Q : Polynomial ℤ} (hQ : Q.IsPrimitive) (hD : Q.discr ≠ 0) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : rootCount Q (p ^ ν) ≤ max Q.natDegree (Q.discr.natAbs ^ 3)