Integral normalization of a primitive algebraic root

Multiplying a primitive root by the leading coefficient gives an integral primitive generator. Away from primes dividing that coefficient, its monic polynomial has at least as many residue roots as the original polynomial.

theorem NairTenenbaum.rootCount_le_integralNormalization {Q : Polynomial ℤ} (hdeg : 1 ≤ Q.natDegree) {p : ℕ} (hp : Nat.Prime p) (hgood : ¬p ∣ Q.leadingCoeff.natAbs) : rootCount Q p ≤ rootCount Q.integralNormalization p

theorem NairTenenbaum.exists_integralGenerator_of_polynomial {K : Type u_1} [Field K] [NumberField K] {Q : Polynomial ℤ} (hQ : Q ≠ 0) (B : PowerBasis ℚ K) (hroot : (Polynomial.aeval B.gen) Q = 0) (hdeg : Q.natDegree = B.dim) : ∃ (θ : NumberField.RingOfIntegers K) (B' : PowerBasis ℚ K), B'.gen = ↑θ ∧ minpoly ℤ θ = Q.integralNormalization