The good-prime root Euler product is bounded by Dedekind zeta

The coefficient comparison uses actual ideals constructed from residue roots. Distinct prime sets give distinct squarefree moduli, so the finite Euler expansion is a subsum of the convergent ideal-norm series.

theorem NairTenenbaum.rootCount_prime_finset_product (Q : Polynomial ℤ) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : rootCount Q (∏ p ∈ S, p) = ∏ p ∈ S, rootCount Q p

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

theorem NairTenenbaum.minpoly_goodPrimeProduct_le_idealNormDirichlet {K : Type u_1} [Field K] [NumberField K] (θ : NumberField.RingOfIntegers K) (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (hgood : ∀ p ∈ S, ¬p ∣ RingOfIntegers.exponent θ) {σ : ℝ} (hσ : 1 < σ) : ∏ p ∈ S, (1 + ↑(rootCount (minpoly ℤ θ) p) * ↑p ^ (-σ)) ≤ idealNormDirichlet K σ