English
For monic q, the degree of the remainder p %ₘ q is strictly less than the degree of q.
Русский
Для монического q степень остатка p %ₘ q меньше степени q.
LaTeX
$$$ \deg(p \%_{m} q) < \deg q \quad (\operatorname{Monic}(q)) $$$
Lean4
theorem degree_modByMonic_lt [Nontrivial R] : ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), degree (p %ₘ q) < degree q
| p, q, hq =>
letI := Classical.decEq R
if h : degree q ≤ degree p ∧ p ≠ 0 then
by
have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
have := degree_modByMonic_lt (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
grind [divModByMonicAux, modByMonic]
else
Or.casesOn (not_and_or.1 h)
(by
unfold modByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_neg h]
exact lt_of_not_ge)
(by
intro hp
unfold modByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero)))
termination_by p => p
