mod_def — Mathlib

English

Let p and q be polynomials over a field. Then the remainder of p upon division by q equals the remainder of p modulo the monic version of q, namely q · C(leadingCoeff(q))^{-1}. Equivalently, p % q = p %_m (q · C(leadingCoeff(q))^{-1}).

Русский

Пусть p и q — многочлены над полем. Остаток от деления p на q равен остатку от деления p по моническому q, то есть по q · C(leadCoeff(q))^{-1}. Иными словами, p % q = p %_{м} (q · C(leadCoeff(q))^{-1}).

LaTeX

$$$ p \bmod q = p \bmod_{\mathrm{monic}}\Bigl(q \cdot C\bigl(\operatorname{leadingCoeff}(q)\bigr)^{-1}\Bigr) $$$

Lean4

theorem mod_def : p % q = p %ₘ (q * C (leadingCoeff q)⁻¹) :=
  rfl

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