the degree of a multivariate polynomial with respect to a monomial ordering

Given a monomial order with bot, notation for the corresponding strict order relation on WithBot (σ →₀ ℕ)

Given a monomial order with bot, notation for the corresponding order relation on WithBot (σ →₀ ℕ)

Given a multivariate polynomial f and a set B of multivariate polynomials over R. A polynomial r is called a remainder of f on division by B with respect to a monomial order m, if there exists g : B →₀ R[X] and a polynomial r s.t.

1. Finite linear combination: f = ∑ (g(b) * b) + r;

2. Degree condition: For eacho b ∈ B, the degree (with bot) of g(b) * b ≤ the degree (with bot) of f w.r.t. m;

3. Remainder irreducibility: No term of r is divisible by the leading monomial of any non-zero b ∈ B.

The definition of remainder makes sense when R is a communitive ring and any polynomial in B either has an invertible leading coefficient or is 0. See the implementation note for the formalization unaligned with the informal definition when not in this case.

A subset G of an ideal I is said to be a Gröbner basis if:

1. G is contained in I (i.e., all polynomials in G belong to the ideal I).

2. The ideal generated by the leading terms of all polynomials in I is equal to the ideal generated by the leading terms of the polynomials in G.