Eventual equality of prime root counts and prime-norm ideal counts

The field generated by a root of an irreducible polynomial supplies the ideal counts. Integral normalization and the conductor exclude only finitely many primes.

theorem NairTenenbaum.exists_irreducible_prime_ideal_match {Q : Polynomial ℤ} [h : Fact (Irreducible (Polynomial.map (Int.castRingHom ℚ) Q))] : ∃ (N : ℕ), ∀ (p : ℕ), Nat.Prime p → N < p → rootCount Q p = idealNormCount (AdjoinRoot (Polynomial.map (Int.castRingHom ℚ) Q)) p