ideal_cofactors : (term -> num) * (num -> term) * conv * term * term * term * term * term * term * term * thm * (term -> thm) -> term list -> term -> term list
SYNOPSIS
Generic procedure to compute cofactors for ideal membership.
DESCRIPTION
The ideal_cofactors function takes first the same set of arguments as RING,
defining a suitable ring for it to operate over. (See the entry for RING for
details.) It then yields a function that given a list of terms [p1; ...; pn]
and another term p, all of which have the right type to be considered as
polynomials over the ring, attempts to find a corresponding set of `cofactors'
[q1; ...; qn] such that the following is an algebraic ring identity:
p = p1 * q1 + ... + pn * qn
That is, it provides a concrete certificate for the fact that p is in the
ideal generated by the p1,...,pn. If p is not in this ideal, the function
will fail.
FAILURE CONDITIONS
Fails if the `polynomials' are of the wrong type, or if ideal membership does
not hold.
EXAMPLE
For an example of the real-number instantiation in action, see
real_ideal_cofactors.