ideal_cofactors : (term -> num) * (num -> term) * conv * term * term * term * term * term * term * term * thm * (term -> thm) -> term list -> term -> term list

Generic procedure to compute cofactors for ideal membership.

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.

Fails if the `polynomials' are of the wrong type, or if ideal membership does not hold.

For an example of the real-number instantiation in action, see real_ideal_cofactors.

real_ideal_cofactors, RING, RING_AND_IDEAL_CONV.