We need two more definitions (Definition 4, p. 82 of Cox, Little, and O'Shea).
(Note that we are inverting the leading coefficients here as well.)
For example, let and with
tdeg (graded reverse lexicographic) order. Then
The idea of an S-polynomial is that leading terms are cancelled. It turns out that every kind of cancellation can be expressed as a sequence of these S-polynomial combinations.
Definition of a Gröbner Basis (Theorem 6 in Cox, Little, and O'Shea, p. 84.)
Let I be a polynomial ideal. Then a basis for I is a Gröbner basis for I if and only if for all pairs , the remainder on division of by G (listed in some order) is zero.
This is a computationally verifiable definition---to test if a given basis is a Gröbner basis, form all S-polynomials, and compute the remainders modulo G. If any of these remainders are nonzero, it isn't a Gröbner basis.