Let \(f: \alpha \to \beta \) be a function and \(s \subseteq \alpha \) a subset with finite image \(f(s)\). Then there exists a finite subset \(s' \subseteq _{\text{fin}} s\) such that:

• \(s' \subseteq s\) (subset relation)

• \(f(s') = f(s)\) (image equality)

• \(|s'| = |f(s)|\) (cardinality preservation)

a Partially Ordered Set, a ≥0

Let \(p \in R[\mathbf{X}]\), \(G'' \subseteq R[\mathbf{X}]\) be a set of polynomials, and \(r \in R[\mathbf{X}]\). Then \(r\) is a remainder of \(p\) modulo \(G''\) with respect to monomial order \(m\) if and only if there exists a finite linear combination from \(G''\) such that:

1. The support of the combination is contained in \(G''\)

2. \(p\) decomposes as the sum of this combination and \(r\)

3. For each \(g' \in G''\), the degree of \(g' \cdot (coefficient\ of\ g')\) is bounded by \(\deg _m(p)\)

4. No term of \(r\) is divisible by any leading term of non-zero elements in \(G''\)

Let \(p, r \in k[x_i : i \in \sigma ]\), and let \(G' \subseteq k[x_i : i \in \sigma ]\) be a finite set. We say that \(r\) is a generalized remainder of \(p\) upon division by \(G'\) if the following two conditions hold:

1. For every nonzero \(g \in G'\) and every monomial \(x^s \in \operatorname {supp}(r)\), there exists some component \(j \in \sigma \) such that

   \[ \operatorname {multideg}(g)_j {\gt} s_j. \]

2. There exists a function \(q : G' \to k[x_i : i \in \sigma ]\) such that:

- For every $g \in G'$,
      $$
      \operatorname{multideg}''(q(g)g) \leq \operatorname{multideg}''(p);
      $$
- The decomposition holds:
      $$
      p = \sum_{g \in G'} q(g)g + r.
      $$

Let \(p \in R[\mathbf{X}]\) be a multivariate polynomial. Then the leading term of \(p\) vanishes with respect to monomial order \(m\) if and only if \(p\) is the zero polynomial:

For any set of polynomials \(G'' \subseteq R[\mathbf{X}]\) and monomial order \(m\), the image of leading terms on the nonzero elements of \(G''\) equals the image on all elements minus zero:

Let \(p \in R[\mathbf{X}]\) be a polynomial, \(G'' \subseteq R[\mathbf{X}]\) a set of polynomials, and \(r \in R[\mathbf{X}]\) a remainder. Then the remainder property is invariant under inserting the zero polynomial:

Let \(p \in R[\mathbf{X}]\) be a polynomial, \(G'' \subseteq R[\mathbf{X}]\) a set of polynomials, and \(r \in R[\mathbf{X}]\) a remainder. Then the remainder property is invariant under removal of the zero polynomial:

the S-polynomial of \(f\) and \(g\) is antisymmetric:

For any polynomial \(g \in \operatorname{MvPolynomial}{\sigma }{R}\) and monomial order \(m\), the S-polynomial with zero as first argument vanishes:

For any polynomial \(g \in \operatorname{MvPolynomial}{\sigma }{R}\) and monomial order \(m\), the S-polynomial with zero as second argument vanishes:

A subset \(s \subseteq R\) has finitely generated span if and only if: \(\exists \) finite \(s' \subseteq s\) such that \(\mathsf{span}(s) = \mathsf{span}(s')\)

For any ring \(R\), the span of the zero singleton set equals the zero submodule:

For any subset \(s \subseteq R\) of a ring \(R\), inserting zero does not change the linear span:

For any subset \(s \subseteq R\) of a ring \(R\), removing zero does not change the linear span:

Let \(G'' \subseteq R[x_1, \dots , x_n]\) be a set of polynomials such that

Then,

Let \(G'' \subseteq R[x_1, \dots , x_n]\), let \(I \subseteq R[x_1, \dots , x_n]\) be an ideal, and let \(p, r \in R[x_1, \dots , x_n]\). Suppose that:

• \(G'' \subseteq I\),

• \(r \in I\),

• \(r\) is the remainder of \(p\) upon division by \(G''\).

Then,

Let \(R\) be a commutative ring, and let \(G'' \subseteq R[x_1, \dots , x_n]\), \(I \subseteq R[x_1, \dots , x_n]\) be an ideal, and \(p, r \in R[x_1, \dots , x_n]\). Assume that:

• \(G'' \subseteq I\),

• \(r\) is the remainder of \(p\) upon division by \(G''\).

Then,

Let \(I \subseteq k[x_i : i \in \sigma ]\) be an ideal, and let \(G \subseteq I\) be a finite subset. Suppose that \(r_1\) and \(r_2\) are generalized remainders of a polynomial \(p\) upon division by \(G\). Then,

Let \(f, h_1, \dots , h_m \in k[\mathbf{x}] \setminus \{ 0\} \), and suppose

If

then

Furthermore, if \(S(h_i, h_j) \ne 0\), then \(\mathrm{lm}(h_i) {\gt} \mathrm{lm}(S(h_i, h_j))\).

\(h_1, h_2 \in k[\mathbf{x}], lm(h_1) = lm(h_2), S(h_1, h_2) \ne 0\), then \(lm(S(h_1, h_2)) {\lt} lm(h_1)\).