MvPolynomial.C_dvd_iff_zmod

theorem MvPolynomial.C_dvd_iff_zmod : ∀ {σ : Type u_1} (n : ℕ) (φ : MvPolynomial σ ℤ), MvPolynomial.C ↑n ∣ φ ↔ (MvPolynomial.map (Int.castRingHom (ZMod n))) φ = 0

This theorem states that for any multivariate polynomial `φ` with integer coefficients and any natural number `n`, the constant polynomial with value `n` divides `φ` if and only if the polynomial `φ` becomes zero when its coefficients are considered modulo `n`. In other words, if we map the polynomial `φ` across the ring homomorphism that casts integers to integers modulo `n`, the resulting polynomial is zero if and only if the original polynomial `φ` is divisible by the constant polynomial `n`.

More concisely: For a multivariate polynomial `φ` with integer coefficients and natural number `n`, `φ` is divisible by the constant polynomial `n` if and only if `φ` evaluates to zero when coefficients are reduced modulo `n`.