Removing fixed prime divisors on finitely many progressions

For a polynomial with nonzero discriminant, the primitive part of every restriction modulo degree! * |discriminant| has no fixed prime divisor.

theorem NairTenenbaum.affineRestriction_natDegree_le (Q : Polynomial ℤ) (M a : ℤ) : (affineRestriction Q M a).natDegree ≤ Q.natDegree

theorem NairTenenbaum.affineRestriction_primPart_reduction_degree_le_one {Q : Polynomial ℤ} (hdeg : 2 ≤ Q.natDegree) {p : ℕ} (hp : Nat.Prime p) {M a : ℤ} {m : ℕ} (hMp : ↑p ^ m ∣ M) (hM : ¬↑p ^ (m + 1) ∣ M) (hD : ¬↑p ^ m ∣ Q.discr) : (Polynomial.map (Int.castRingHom (ZMod p)) (affineRestriction Q M a).primPart).natDegree ≤ 1

noncomputable def NairTenenbaum.fixedPrimeRemovalModulus (Q : Polynomial ℤ) : ℕ

The progression modulus used to remove fixed prime divisors.

Equations

• NairTenenbaum.fixedPrimeRemovalModulus Q = Q.natDegree.factorial * Q.discr.natAbs

theorem NairTenenbaum.fixedPrimeRemovalModulus_pos {Q : Polynomial ℤ} (hD : Q.discr ≠ 0) : 0 < fixedPrimeRemovalModulus Q

theorem NairTenenbaum.affine_primPart_noFixedPrimeDivisor {Q : Polynomial ℤ} (hD : Q.discr ≠ 0) (a : ℤ) : NoFixedPrimeDivisor (affineRestriction Q (↑(fixedPrimeRemovalModulus Q)) a).primPart