English
For polynomials p and q, if q is monic then p /ₘ q is the quotient of p by q; otherwise it is 0.
Русский
Для многочленов p, q: если q монический, то p /ₘ q — частное деления; иначе 0.
LaTeX
$$$ p /_{m} q = \begin{cases} \text{quotient}(p,q) & \text{если } \operatorname{Monic}(q) \\ 0 & \text{иначе} \end{cases} $$$
Lean4
/-- `divByMonic`, denoted as `p /ₘ q`, gives the quotient of `p` by a monic polynomial `q`. -/
def divByMonic (p q : R[X]) : R[X] :=
letI := Classical.decEq R
if hq : Monic q then (divModByMonicAux p hq).1 else 0