REAL_IDEAL_CONV : term list -> term -> thm
Produces identity proving ideal membership over the reals.
The call REAL_IDEAL_CONV [`p1`; ...; `pn`] `p`, where all the terms have
type :real and can be considered as polynomials, will test whether p is in
the ideal generated by the p1,...,pn. If so, it will return a corresponding
theorem |- p = q1 * p1 + ... + qn * pn showing how to express p in terms of
the other polynomials via some `cofactors' qi.
- FAILURE CONDITIONS
Fails if the terms are ill-typed, or if ideal membership fails.
In the case of a singleton list, this just corresponds to dividing one
multivariate polynomial by another, e.g.
# REAL_IDEAL_CONV [`x - &1`] `x pow 4 - &1`;;
1 basis elements and 0 critical pairs
val it : thm =
|- x pow 4 - &1 = (&1 * x pow 3 + &1 * x pow 2 + &1 * x + &1) * (x - &1)
- SEE ALSO
ideal_cofactors, real_ideal_cofactors, REAL_RING, RING, RING_AND_IDEAL_CONV.