div_def — Mathlib

English

The division of polynomials is defined by the same monic decomposition formula as before: p / q = C(leadingCoeff q)⁻¹ · (p /ₘ (q · C(leadingCoeff q)⁻¹)).

Русский

Деление многочленов определяется той же формулой разложения на монический множитель.

LaTeX

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

Lean4

theorem div_def : p / q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹)) :=
  rfl

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