English
For polynomials p, q ∈ R[X], cancelLeads(p,q) is formed by multiplying p and q by monomials to align their leading terms and then subtracting.
Русский
Для многочленов p, q ∈ R[X] cancelLeads(p,q) получает результат умножением p и q на подходящие мономы, чтобы выровнять ведущие члены, затем вычитанием.
LaTeX
$$$p\\,\\cancelLeads\\,q = C(p.leadingCoeff) \\cdot X^{(p.natDegree-q.natDegree)} \\cdot q - C(q.leadingCoeff) \\cdot X^{(q.natDegree-p.natDegree)} \\cdot p.$$$
Lean4
/-- `cancelLeads p q` is formed by multiplying `p` and `q` by monomials so that they
have the same leading term, and then subtracting. -/
def cancelLeads : R[X] :=
C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) * q - C q.leadingCoeff * X ^ (q.natDegree - p.natDegree) * p
