that we allow $G$ to be a monoid rather than a group. Indeed, the image of $G$ in the monoid of injective maps ${\mathrm{Mon}}\to {\mathrm{Mon}}$ contains no other invertible elements than the identity: If $\pi \in G$ then $\pi m \geq m$ since otherwise $m>\pi m>\pi^2 m>\ldots$ would be an infinite strictly decreasing chain. But then if (the image of) $\pi$ is invertible, we have $\pi m>m>\pi^{-1}m>\pi^{-2}m>\ldots$, another infinite decreasing chain.

We set out to translate familiar notions from the setting of ordinary Gröbner bases to our equivariant setting. In what follows the coeffient in $f$ of ${\mathrm{lm}}(f)$, the [*leading coefficient*]{}, is denoted ${\mathrm{lc}}(f)$, and ${\mathrm{lt}}(f)={\mathrm{lc}}(f) {\mathrm{lm}}(f)$ is the [*leading term*]{} of $f$.

\[lm:GBgenerates\] If $I$ is $G$-stable and $B$ is a $G$-Gröbner basis of $I$, then $GB=\{\pi b \mid \pi \in G,\ b \in B\}$ generates the ideal $I$.

If not, then take an $f \in I \setminus {\langle}GB {\rangle}$ with ${\mathrm{lm}}(f)$ minimal. Take $b \in B$ and $\pi \in G$ with ${\mathrm{lm}}(\pi b)|{\mathrm{lm}}(f)$. Subtracting $({\mathrm{lt}}(f)/{\mathrm{lt}}(\pi b)) \pi b$ from $f$ yields an element in $I\setminus {\langle}GB {\rangle}$ with leading term strictly smaller than that of $f$, a contradiction.

Given $f \in K[X]$ and $B \subseteq K[X]$, proceed as 