English
p %ₘ q + q · (p /ₘ q) = p.
Русский
p %ₘ q + q · (p /ₘ q) = p.
LaTeX
$$$ p \%_{m} q + q \cdot (p /_{m} q) = p $$$
Lean4
theorem modByMonic_eq_sub_mul_div : ∀ (p : R[X]) {q : R[X]} (_hq : Monic q), p %ₘ q = p - q * (p /ₘ q)
| p, q, hq =>
letI := Classical.decEq R
if h : degree q ≤ degree p ∧ p ≠ 0 then by
have _wf := div_wf_lemma h hq
have ih := modByMonic_eq_sub_mul_div (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
unfold modByMonic divByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_pos h]
rw [modByMonic, dif_pos hq] at ih
refine ih.trans ?_
unfold divByMonic
rw [dif_pos hq, dif_pos hq, if_pos h, mul_add, sub_add_eq_sub_sub]
else by
unfold modByMonic divByMonic divModByMonicAux
dsimp
rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]
termination_by p => p
