mod — Mathlib

English

There is a division operation on the polynomial ring R[X] making it a division algebra when R is a field.

Русский

Для кольца многочленов R[X] существует операция деления, делающая его делимой структурой над полем R.

LaTeX

$$$\text{instance: } \mathrm{Div}(\,\mathbb{R}[X]\,)\,=\, \langle \text{div} \rangle.$$$

Lean4

/-- Remainder of polynomial division. See `Polynomial.modByMonic` for more details. -/
def mod (p q : R[X]) :=
  p %ₘ (q * C (leadingCoeff q)⁻¹)

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