English
There exists a division procedure by a monic q: for any p, there is a pair (quotient, remainder) such that p = q · quotient + remainder and the remainder has strictly smaller degree than q.
Русский
Существуют полиномы частного и остатка при делении по моническому q: p = q·quotient + remainder и deg(remainder) < deg(q).
LaTeX
$$$ \exists (\text{quot}, \text{rem}) = \text{divModByMonicAux}(p, q)\; (q\text{ мононичен}):\; p = q \cdot \text{quot} + \text{rem} \land \deg(\text{rem}) < \deg(q) $$$
Lean4
/-- See `divByMonic`. -/
noncomputable def divModByMonicAux : ∀ (_p : R[X]) {q : R[X]}, Monic q → R[X] × R[X]
| p, q, hq =>
letI := Classical.decEq R
if h : degree q ≤ degree p ∧ p ≠ 0 then
let z := C (leadingCoeff p) * X ^ (natDegree p - natDegree q)
have _wf := div_wf_lemma h hq
let dm := divModByMonicAux (p - q * z) hq
⟨z + dm.1, dm.2⟩
else ⟨0, p⟩
termination_by p => p
