modByMonic_eq_of_dvd_sub — Mathlib

English

If q is monic and q ∣ (p1 − p2), then p1 mod q = p2 mod q.

Русский

Если q моноик и q делит (p1 − p2), тогда p1 mod q = p2 mod q.

LaTeX

$$$ q.Monic \rightarrow (q \mid (p_1 - p_2)) \Rightarrow p_1 \bmod q = p_2 \bmod q $$$

Lean4

theorem modByMonic_eq_of_dvd_sub (hq : q.Monic) (h : q ∣ p₁ - p₂) : p₁ %ₘ q = p₂ %ₘ q :=
  by
  nontriviality R
  obtain ⟨f, sub_eq⟩ := h
  refine (div_modByMonic_unique (p₂ /ₘ q + f) _ hq ⟨?_, degree_modByMonic_lt _ hq⟩).2
  rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, modByMonic_add_div _ hq, add_comm]

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