English
The remainder of p upon division by monic q is zero if and only if q divides p.
Русский
Остаток от деления p на моному q равен нулю тогда и только тогда, когда q делит p.
LaTeX
$$$$ p \\%ₘ q = 0 \\quad\\Leftrightarrow\\quad q \\mid p. $$$$
Lean4
theorem modByMonic_eq_zero_iff_dvd (hq : Monic q) : p %ₘ q = 0 ↔ q ∣ p :=
⟨fun h => by rw [← modByMonic_add_div p hq, h, zero_add]; exact dvd_mul_right _ _, fun h =>
by
nontriviality R
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h
by_contra hpq0
have hmod : p %ₘ q = q * (r - p /ₘ q) := by rw [modByMonic_eq_sub_mul_div _ hq, mul_sub, ← hr]
have : degree (q * (r - p /ₘ q)) < degree q := hmod ▸ degree_modByMonic_lt _ hq
have hrpq0 : leadingCoeff (r - p /ₘ q) ≠ 0 := fun h =>
hpq0 <| leadingCoeff_eq_zero.1 (by rw [hmod, leadingCoeff_eq_zero.1 h, mul_zero, leadingCoeff_zero])
have hlc : leadingCoeff q * leadingCoeff (r - p /ₘ q) ≠ 0 := by rwa [Monic.def.1 hq, one_mul]
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree (mt leadingCoeff_eq_zero.2 hrpq0)] at this
exact not_lt_of_ge (Nat.le_add_right _ _) (WithBot.coe_lt_coe.1 this)⟩
