C_dvd_iff_zmod — Mathlib

English

A polynomial with integer coefficients is divisible by n if and only if its image in ZMod n is zero.

Русский

Полином с целочисленными коэффициентами делится на n тогда и только тогда его образ в ZMod n равен нулю.

LaTeX

$$C (n) ∣ φ ↔ map (Int.castRingHom (ZMod n)) φ = 0$$

Lean4

/-- A polynomial over the integers is divisible by `n : ℕ`
if and only if it is zero over `ZMod n`. -/
theorem C_dvd_iff_zmod (n : ℕ) (φ : MvPolynomial σ ℤ) : C (n : ℤ) ∣ φ ↔ map (Int.castRingHom (ZMod n)) φ = 0 :=
  C_dvd_iff_map_hom_eq_zero _ _ (CharP.intCast_eq_zero_iff (ZMod n) n) _

Похожие утверждения