Reduction of integer polynomials modulo n

An integer polynomial reduces to zero in (ZMod n)[X] exactly when n divides every one of its coefficients, that is, when the constant n divides it in ℤ[X]. Consequently two integer polynomials with the same reduction modulo n differ by n times an integer polynomial, and if the reduction of Φ divides the reduction of G then G = Φ Q + n D for integer polynomials Q and D. Conversely, for a prime p, if Φ reduces to an irreducible polynomial and Φ(x) and G(x) lie in a proper ideal containing p, then the reduction of Φ divides the reduction of G.

Main results

• Polynomial.map_intCastRingHom_zmod_eq_zero_iff: G.map (Int.castRingHom (ZMod n)) = 0 exactly when (n : ℤ[X]) ∣ G.
• Polynomial.exists_C_mul_eq_sub_of_map_zmod_eq: polynomials with the same reduction modulo n differ by C n * D.
• Polynomial.exists_eq_mul_add_C_mul_of_map_zmod_dvd: if Φ mod n divides G mod n, then G = Φ * Q + C n * D.
• Polynomial.map_zmod_dvd_map_of_aeval_mem: if Φ mod p is irreducible and Φ(x), G(x) lie in a proper ideal containing the prime p, then Φ mod p divides G mod p.

@[simp]

theorem Polynomial.map_intCastRingHom_zmod_eq_zero_iff {n : ℕ} (G : Polynomial ℤ) : map (Int.castRingHom (ZMod n)) G = 0 ↔ ↑n ∣ G

An integer polynomial reduces to zero modulo n exactly when n divides it, that is, when n divides each of its coefficients.

theorem Polynomial.exists_C_mul_eq_sub_of_map_zmod_eq {n : ℕ} {G G' : Polynomial ℤ} (h : map (Int.castRingHom (ZMod n)) G = map (Int.castRingHom (ZMod n)) G') : ∃ (D : Polynomial ℤ), C ↑n * D = G - G'

Two integer polynomials with the same reduction modulo n differ by n times an integer polynomial.

theorem Polynomial.exists_eq_mul_add_C_mul_of_map_zmod_dvd {n : ℕ} {Φ G : Polynomial ℤ} (h : map (Int.castRingHom (ZMod n)) Φ ∣ map (Int.castRingHom (ZMod n)) G) : ∃ (Q : Polynomial ℤ) (D : Polynomial ℤ), G = Φ * Q + C ↑n * D

If the reduction of Φ modulo n divides the reduction of G, then G = Φ Q + n D for integer polynomials Q and D.

theorem Polynomial.map_zmod_dvd_map_of_aeval_mem {A : Type u_1} [CommRing A] {p : ℕ} [Fact (Nat.Prime p)] (x : A) {P : Ideal A} (hP : P ≠ ⊤) (hp : ↑p ∈ P) {Φ G : Polynomial ℤ} (hirr : Irreducible (map (Int.castRingHom (ZMod p)) Φ)) (hΦ : (aeval x) Φ ∈ P) (hG : (aeval x) G ∈ P) : map (Int.castRingHom (ZMod p)) Φ ∣ map (Int.castRingHom (ZMod p)) G

Let p be a prime, let x be an element of a commutative ring A, and let P be a proper ideal of A containing p. If Φ reduces modulo p to an irreducible polynomial and both Φ(x) and G(x) lie in P, then the reduction of Φ divides the reduction of G.