divByMonic — Mathlib

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

Похожие утверждения