Linear relations between polynomials over a field #
A relation A * q + B * p = 0 between polynomials over a field says that A * q is divisible by
p; dividing by the gcd of p and q leaves coprime quotients, so in fact p / gcd p q divides
A. So a nonzero A in such a relation has degree at least deg p - deg (gcd p q): this is the
degree bound behind the nonvanishing of the principal subresultant coefficient at the degree of
the gcd.
theorem
Polynomial.eq_zero_of_mul_add_mul_eq_zero_of_degree_lt
{K : Type u_1}
[Field K]
[DecidableEq K]
{p q A B : Polynomial K}
(hp : p ≠ 0)
(hAB : A * q + B * p = 0)
(hA : A.degree < ↑(p.natDegree - (EuclideanDomain.gcd p q).natDegree))
:
In a relation A * q + B * p = 0 with p ≠ 0, if A has degree below
deg p - deg (gcd p q), then A = 0: dividing by the gcd leaves coprime quotients, so
p / gcd p q divides A.