English
The remainder of p modulo a monic q is p when q is not monic; otherwise it is the standard remainder from division by a monic divisor.
Русский
Остаток от деления p по модулю монического q равен p, если q не моническое; иначе — обычный остаток от деления по моническому делителю.
LaTeX
$$$ p \%_{m} q = p \quad \text{если } \neg\operatorname{Monic}(q) $, \\ $ p \%_{m} q = \text{remainder from division by } q \text{ и } \operatorname{Monic}(q). $$$
Lean4
/-- `modByMonic`, denoted as `p %ₘ q`, gives the remainder of `p` by a monic polynomial `q`. -/
def modByMonic (p q : R[X]) : R[X] :=
letI := Classical.decEq R
if hq : Monic q then (divModByMonicAux p hq).2 else p
