div — Mathlib

English

The division of polynomials can be expressed via monic division: p / q = C(leadingCoeff q)⁻¹ · (p /ₘ (q · C(leadingCoeff q)⁻¹)).

Русский

Деление многочленов определяется через деление на монический множитель: p/q = C(leadCoeff q)⁻¹ · (p /ₘ (q · C(leadCoeff q)⁻¹)).

LaTeX

$$$p/q = C(\operatorname{leadingCoeff}(q))^{-1} \cdot \left(p /_{m} \bigl(q \cdot C(\operatorname{leadingCoeff}(q))^{-1}\bigr)\right).$$$

Lean4

/-- Division of polynomials. See `Polynomial.divByMonic` for more details. -/
def div (p q : R[X]) :=
  C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹))

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